let A, B be Ordinal; :: thesis: for R being Relation st A in B holds
ClosedProd (R,A,A) = OpenProd (R,A,B)
let R be Relation; :: thesis: ( A in B implies ClosedProd (R,A,A) = OpenProd (R,A,B) )
assume A1: A in B ; :: thesis: ClosedProd (R,A,A) = OpenProd (R,A,B)
then A2: ClosedProd (R,A,A) c= ClosedProd (R,A,B) by Th17, ORDINAL1:def 2;
ClosedProd (R,A,B) c= ClosedProd (R,A,A)

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in ClosedProd (R,A,B) or [x,y] in ClosedProd (R,A,A) )
assume A3: [x,y] in ClosedProd (R,A,B) ; :: thesis: [x,y] in ClosedProd (R,A,A)
A4: ( x in Day (R,A) & y in Day (R,A) ) by A3, ZFMISC_1:87;
then A5: ( born (R,x) c= A & born (R,y) c= A ) by Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by A4, A3, Def10;
hence [x,y] in ClosedProd (R,A,A) by A4, A5, Def10; :: thesis: verum

end;

then A6: ClosedProd (R,A,B) = ClosedProd (R,A,A) by A2, XBOOLE_0:def 10;
A7: ClosedProd (R,A,B) c= OpenProd (R,A,B) by A1, Th19;
OpenProd (R,A,B) c= ClosedProd (R,A,B) by Th16;
hence ClosedProd (R,A,A) = OpenProd (R,A,B) by A6, A7, XBOOLE_0:def 10; :: thesis: verum