let A, B be Ordinal; :: thesis: for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))
let R, S be Relation; :: thesis: ( R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) implies R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) )
assume A1: ( R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis: R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

per cases ( B c= A or A in B ) by ORDINAL1:16;

suppose B c= A ; :: thesis: R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

then ( R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B)) & S /\ (ClosedProd (S,A,B)) c= R /\ (ClosedProd (R,A,B)) ) by A1, Lm2;
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by XBOOLE_0:def 10; :: thesis: verum

end;

suppose A in B ; :: thesis: R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

then ( ClosedProd (R,A,B) c= OpenProd (R,A,B) & OpenProd (R,A,B) c= ClosedProd (R,A,B) & ClosedProd (S,A,B) c= OpenProd (S,A,B) & OpenProd (S,A,B) c= ClosedProd (S,A,B) ) by Th16, Th19;
then ( ClosedProd (R,A,B) = OpenProd (R,A,B) & ClosedProd (S,A,B) = OpenProd (S,A,B) ) by XBOOLE_0:def 10;
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by A1; :: thesis: verum

end;

end;