let A, B be Ordinal; :: thesis: ( A c< B or A = B or B c< A )
assume ( not A c< B & not A = B & not B c< A ) ; :: thesis: contradiction
then ( not A c= B & not B c= A ) by XBOOLE_0:def 8;
hence contradiction ; :: thesis: verum