let A, B be Ordinal; :: thesis: for R being Relation holds OpenProd (R,A,B) c= ClosedProd (R,A,B)
let R be Relation; :: thesis: OpenProd (R,A,B) c= ClosedProd (R,A,B)
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in OpenProd (R,A,B) or [x,y] in ClosedProd (R,A,B) )
assume A1: [x,y] in OpenProd (R,A,B) ; :: thesis: [x,y] in ClosedProd (R,A,B)
then A2: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A1, Def9;
then ( ( 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 ORDINAL1:def 2;
hence [x,y] in ClosedProd (R,A,B) by A2, Def10; :: thesis: verum