let A, B be Ordinal; :: thesis: ( A c< B or A = B or B c< A )
assume that
A1: ( not A c< B & not A = B ) and
A2: not B c< A ; :: thesis: contradiction
not A c= B by A1;
hence contradiction by A2; :: thesis: verum