let X be set ; :: thesis: ( ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) implies X is ordinal )
assume A1: for x being set st x in X holds
( x is Ordinal & x c= X ) ; :: thesis: X is ordinal
thus X is epsilon-transitive :: according to ORDINAL1:def 4 :: thesis: X is epsilon-connected

proof

let x be set ; :: according to ORDINAL1:def 2 :: thesis: ( x in X implies x c= X )
assume x in X ; :: thesis: x c= X
hence x c= X by A1; :: thesis: verum

end;

let x be set ; :: according to ORDINAL1:def 3 :: thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; :: thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume ( x in X & y in X ) ; :: thesis: ( x in y or x = y or y in x )
then ( x is Ordinal & y is Ordinal ) by A1;
hence ( x in y or x = y or y in x ) by Th24; :: thesis: verum