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