Definicja

start

Definicja zaczyna się od słowa kluczowego definition, a kończy się słowem end. Definicja zawiera deklarację locusów?, ewentualne złożenia i właściwą definicję lub redefinicję. Poza tym warunki poprawności i ewentualne własności.

definition
  let X be set;
  mode Element of X means
  it in X if X is non empty otherwise it is empty;
  existence by XBOOLE_0:def 1;
  consistency;
  sethood
  proof
   per cases;
   case X is non empty;
    take X;
    thus thesis;
   end;
   case X is empty;
    take {{}};
    let y be set;
    thus thesis by TARSKI:def 1;
   end;
  end;
end;

Definicja elementu zbioru jest przez przypadki: gdy zbiór jest niepusty oraz gdy jest pusty. Stąd warunek poprawności consistency -- jak przypadki się pokrywają, to odpowiadające im definiensy cząstkowe są równoważne. Warunek existence stwierdza istnienie zbioru spełniającego definiens. Udowodniona została własność sethood mówiąca o istnieniu uniwersum definiowanego typu.

definition
  let x be Θ;
  attr x is ξ means Φ(x);
end;

definition
  let x be Θ;
  attr x is ξ means Φ1(x) if  α1(x),
          .......
         Φn(x) if  αn(x)
         otherwise Φn+1(x);
end;

definition
  let x be Θ;
  redefine attr x is ξ means Φ'(x);
end;

definition
  let x be Θ;
  mode Θ of x -> Θ' of x means Φ(x,it)
end;

definition
  let x be Θ;
  func ⊕ x -> Θ of x means Φ(x,it);
end;

definition
  let x be Θ;
  func ⊕ x -> Θ of x equals τ(x);
end;

definition
  let x be Θ;
  redefine func ⊕ x -> Θ' of x;
end;

definition
  let x be Θ;
  redefine func ⊕ x means Φ'(x);
end;

definition
  let x be Θ;
  pred ≈ x ->  means Φ(x);
end;

definition
  let x be Θ;
  pred ≈ x means Φ1(x) if  α1(x),
          .......
         Φn(x) if  αn(x)
         otherwise Φn+1(x);
end;

definition
  let x be Θ;
  redefine pred ≈ x means Φ'(x);
end;