given X being set such that A1: for x being set holds
( x in X iff x is Ordinal ) ; :: thesis: contradiction
A2: X is epsilon-transitive

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
then A3: x is Ordinal by A1;
thus x c= X :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in X )
assume a in x ; :: thesis: a in X
then a is Ordinal by A3, Th9;
hence a in X by A1; :: thesis: verum

end;

end;

X is epsilon-connected

proof

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 Th10; :: thesis: verum

end;

then X in X by A1, A2;
hence contradiction ; :: thesis: verum