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

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