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