let A, B be Ordinal; :: thesis: ( A c= B implies No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) )
set R = No_Ord A;
set S = No_Ord B;
assume A c= B ; :: thesis: No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A))
then A1: ClosedProd ((No_Ord B),A,A) c= ClosedProd ((No_Ord B),B,B) by Th30;
A2: ( [:(Day ((No_Ord B),B)),(Day ((No_Ord B),B)):] = ClosedProd ((No_Ord B),B,B) & [:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) ) by Lm3;
then No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),B,B) by Def12;
then ( No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),A,A) & No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),A,A) ) by A2, A1, Def12;
then A3: (No_Ord A) /\ (ClosedProd ((No_Ord A),A,A)) = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) by Th23;
No_Ord A c= ClosedProd ((No_Ord A),A,A) by A2, Def12;
hence No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) by A3, XBOOLE_1:28; :: thesis: verum