let A, B be Ordinal; :: thesis: for a, b being object st a <= No_Ord A,b & a in Day B & b in Day B holds
a <= No_Ord B,b
let a, b be object ; :: thesis: ( a <= No_Ord A,b & a in Day B & b in Day B implies a <= No_Ord B,b )
set R = No_Ord A;
set S = No_Ord B;
assume A1: ( a <= No_Ord A,b & a in Day B & b in Day B ) ; :: thesis: a <= No_Ord B,b
then A2: [a,b] in ClosedProd ((No_Ord B),B,B) by Th33;

per cases ( B c= A or A c= B ) ;

suppose A3: B c= A ; :: thesis: a <= No_Ord B,b

then ClosedProd ((No_Ord B),B,B) = ClosedProd ((No_Ord A),B,B) by Th32;
then No_Ord B = (No_Ord A) /\ (ClosedProd ((No_Ord B),B,B)) by A3, Th34;
hence a <= No_Ord B,b by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A c= B ; :: thesis: a <= No_Ord B,b

then A4: ClosedProd ((No_Ord B),A,A) c= ClosedProd ((No_Ord B),B,B) by Th30;
A5: ( [:(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 A preserves_No_Comparison_on ClosedProd ((No_Ord A),A,A) & 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 A4;
then A6: (No_Ord A) /\ (ClosedProd ((No_Ord A),A,A)) = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) by Th23;
A7: No_Ord A c= ClosedProd ((No_Ord A),A,A) by A5, Def12;
[a,b] in (No_Ord A) /\ (ClosedProd ((No_Ord A),A,A)) by A1, A7, XBOOLE_0:def 4;
hence a <= No_Ord B,b by A6, XBOOLE_0:def 4; :: thesis: verum

end;

end;