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, Th7;
then not A c= B by A2;
then consider a being object such that
A3: ( a in A & not a in B ) ;
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 object holds
( not a in A \ B or not a in X ) by TARSKI:3;
A6: X c= A by A4, Def2;
now :: thesis: for b being object st b in X holds
b in B
let b be object ; :: 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 ;
then A8: ( X c< B or X = B ) ;
( not X in B & X is Ordinal ) by A4, Th9, XBOOLE_0:def 5;
hence B in A by A4, A8, Th7; :: thesis: verum