let A, B be Ordinal; :: thesis: ( A in B or A = B or B in A )
assume that
A1: not A in B and
A2: A <> B ; :: thesis: B in A
not A c< B by A1, Th21;
then not A c= B by A2, XBOOLE_0:def 8;
then consider a being set such that
A3: ( a in A & not a in B ) by TARSKI:def 3;
a in A \ B by A3, XBOOLE_0:def 5;
then consider X being set such that
A4: X in A \ B and
A5: for a being set holds
( not a in A \ B or not a in X ) by TARSKI:2;
A6: X c= A by A4, Def2;

now

let b be set ; :: thesis: ( b in X implies b in B )
assume A7: b in X ; :: thesis: b in B
then not b in A \ B by A5;
hence b in B by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then X c= B by TARSKI:def 3;
then A8: ( X c< B or X = B ) by XBOOLE_0:def 8;
( not X in B & X is Ordinal ) by A4, Th23, XBOOLE_0:def 5;
hence B in A by A4, A8, Th21; :: thesis: verum