let A, B be Ordinal; :: thesis: ( No_uOrdinal_op A < No_uOrdinal_op B iff A in B )
A1: ( No_uOrdinal_op A == No_Ordinal_op A & No_uOrdinal_op B == No_Ordinal_op B ) by Th73;
thus ( No_uOrdinal_op A < No_uOrdinal_op B implies A in B ) :: thesis: ( A in B implies No_uOrdinal_op A < No_uOrdinal_op B )

proof

assume No_uOrdinal_op A < No_uOrdinal_op B ; :: thesis: A in B
then No_Ordinal_op A < No_uOrdinal_op B by A1, SURREALO:4;
then No_Ordinal_op A < No_Ordinal_op B by A1, SURREALO:4;
hence A in B by Th68; :: thesis: verum

end;

assume A in B ; :: thesis: No_uOrdinal_op A < No_uOrdinal_op B
then No_uOrdinal_op A < No_Ordinal_op B by Th68, A1, SURREALO:4;
hence No_uOrdinal_op A < No_uOrdinal_op B by A1, SURREALO:4; :: thesis: verum