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