theorem Th1:
for
X,
Y being
set st
Y in X holds
not
X c= Y
theorem Th4:
for
X,
x being
set holds
(
x in succ X iff (
x in X or
x = X ) )
Lm1:
( {} is epsilon-transitive & {} is epsilon-connected )
theorem Th21:
for
X being
set holds
not for
x being
set holds
(
x in X iff
x is
Ordinal )
theorem
for
x being
set for
n being
Nat st
x in n holds
x is
Nat