begin
theorem Th5:
for
Y,
X being
set st
Y in X holds
not
X c= Y
theorem Th8:
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 Th25:
for
X being
set holds
not for
x being
set holds
(
x in X iff
x is
Ordinal )
begin
:: 4. Definition of ordinal numbers - Ordinal
::