let a be object ; :: thesis: for A being Ordinal st a in A holds
a is Ordinal
let A be Ordinal; :: thesis: ( a in A implies a is Ordinal )
assume A1: a in A ; :: thesis: a is Ordinal
reconsider a = a as set by TARSKI:1;
A2: a c= A by Def2, A1;

now :: thesis: for y being set st y in a holds
y c= a

let y be set ; :: thesis: ( y in a implies y c= a )
assume A3: y in a ; :: thesis: y c= a
then A4: y c= A by A2, Def2;
assume not y c= a ; :: thesis: contradiction
then consider b being object such that
A5: ( b in y & not b in a ) ;
b in y \ a by A5, XBOOLE_0:def 5;
then consider z being set such that
A6: z in y \ a and
for c being object holds
( not c in y \ a or not c in z ) by TARSKI:3;
z in y by A6;
then ( z in a or z = a or a in z ) by A1, A4, Def3;
hence contradiction by A3, A6, XBOOLE_0:def 5, XREGULAR:7; :: thesis: verum

end;

then A7: a is epsilon-transitive ;
for y, z being set st y in a & z in a & not y in z & not y = z holds
z in y by A2, Def3;
then a is epsilon-connected ;
hence a is Ordinal by A7; :: thesis: verum