let A, B be Ordinal; :: thesis: ( No_Ordinal_op A < No_Ordinal_op B iff A in B )
thus ( No_Ordinal_op A < No_Ordinal_op B implies A in B ) :: thesis: ( A in B implies No_Ordinal_op A < No_Ordinal_op B )

proof

assume A1: No_Ordinal_op A < No_Ordinal_op B ; :: thesis: A in B
assume not A in B ; :: thesis: contradiction

per cases then ( A = B or B c< A ) by ORDINAL1:16, XBOOLE_0:def 8;

suppose A = B ; :: thesis: contradiction

hence contradiction by A1, SURREALO:3; :: thesis: verum

end;

suppose B c< A ; :: thesis: contradiction

then No_Ordinal_op B <= No_Ordinal_op A by Lm23, ORDINAL1:11;
hence contradiction by A1; :: thesis: verum

end;

end;

end;

thus ( A in B implies No_Ordinal_op A < No_Ordinal_op B ) by Lm23; :: thesis: verum