let a be set ; :: 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
then A2: a c= A by Def2;

now

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 set such that
A5: ( b in y & not b in a ) by TARSKI:def 3;
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 set holds
( not c in y \ a or not c in z ) by TARSKI:7;
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, Th3, XBOOLE_0:def 5; :: thesis: verum

end;

then A7: a is epsilon-transitive by Def2;
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 by Def3;
hence a is Ordinal by A7; :: thesis: verum