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