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

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 A3;
hence b in B by A5, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then X c= B by TARSKI:def 3;
then ( X c< B or X = B ) by XBOOLE_0:def 8;
hence B in A by A4, A6, Th21; :: thesis: verum