(x=y) ↔ (∀z) ((z∈x) ↔ (z∈y))
   # Mnoziny x a y su si rovne, ked obsahuju prave tie iste prvky.

(x⊆y) ↔ (∀z) ((z∈x) → (z∈y))
   # Mnozina x je podmnozinou mnoziny y, ked vsetky prvky mnoziny x su prvkami mnoziny y.

transitive(x) ↔ (∀z) ((z∈x) → (z⊆x))
   # Mnozina x je tranzitivna, ked kazdy jej prvok je jej podmnozinou.

is_least_element(z,x,R) ↔ (z∈x) ∧ (∀w) ((w∈x) → ((z=w) ∨ (zRw)))
   # Mnozina z je najmensi prvok v x pri usporiadani R, ked je mensi alebo rovny vsetkym ostatnym prvkom.

well_ordered(x,R) ↔ (∀y) (((y⊆x) ∧ (∃z) (z∈y)) → (∃z) is_least_element(z,y,R))
   # Mnozina x je dobre usporiadana usporiadanim R, ked kazda neprazdna podmnozina x ma najmensi prvok.

ordinal(x) ↔ transitive(x) ∧ well_ordered(x,∈)
   # Mnozina x je ordinal, ked je tranzitivna a zaroven dobre usporiadana relaciou nalezenia.

is_successor(s,x) ↔ (∀z) ((z∈s) ↔ ((z∈x) ∨ (z=x)))
   # Mnozina s je naslednik mnoziny x, ked obsahuje mnozinu x, vsetky jej prvky, a nic ine, teda s = x ∪ {x}.

has_predecessor(s,x) ↔ (∃p) ((p∈x) ∧ is_successor(s,p))
   # Mnozina s ma predchodcu v mnozine x, ked v mnozine x existuje prvok, ktoreho naslednik je s.

natural_number(n) ↔ ordinal(n) ∧ ((∀x) ((x∈n) ∧ (∃z) (z∈x)) → has_predecessor(x,n)) ∧ ((∃p) is_successor(n,p))
   # Mnozina n je prirodzene cislo, ked je ordinalom, kazdy jej neprazdny prvok v nej ma predchodcu a mnozina n ma predchodcu.