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;
then for y, z being set st y in a & z in a & not y in z & not y = z holds
z in y by Def3;
then A3: a is epsilon-connected by Def3;

now

let y be set ; :: thesis: ( y in a implies y c= a )
assume A4: y in a ; :: thesis: y c= a
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 & ( for c being set holds
( not c in y \ a or not c in z ) ) ) by TARSKI:7;
A7: ( z in y & not z in a ) by A6, XBOOLE_0:def 5;
y c= A by A2, A4, Def2;
then ( z in a or z = a or a in z ) by A1, A7, Def3;
hence contradiction by A4, A6, Th3, XBOOLE_0:def 5; :: thesis: verum

end;

then a is epsilon-transitive by Def2;
hence a is Ordinal by A3; :: thesis: verum