let A be Ordinal; :: thesis: for R being Relation holds ClosedProd (R,A,A) = [:(Day (R,A)),(Day (R,A)):]
let R be Relation; :: thesis: ClosedProd (R,A,A) = [:(Day (R,A)),(Day (R,A)):]
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in ClosedProd (R,A,A) or [x,y] in [:(Day (R,A)),(Day (R,A)):] ) & ( not [x,y] in [:(Day (R,A)),(Day (R,A)):] or [x,y] in ClosedProd (R,A,A) ) )
thus ( [x,y] in ClosedProd (R,A,A) implies [x,y] in [:(Day (R,A)),(Day (R,A)):] ) ; :: thesis: ( not [x,y] in [:(Day (R,A)),(Day (R,A)):] or [x,y] in ClosedProd (R,A,A) )
assume [x,y] in [:(Day (R,A)),(Day (R,A)):] ; :: thesis: [x,y] in ClosedProd (R,A,A)
then A1: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87;
then A2: ( born (R,x) c= A & born (R,y) c= A ) by Def8;

per cases ( born (R,x) = A or born (R,y) = A or ( born (R,x) <> A & born (R,y) <> A ) ) ;

suppose ( born (R,x) = A or born (R,y) = A ) ; :: thesis: [x,y] in ClosedProd (R,A,A)

hence [x,y] in ClosedProd (R,A,A) by A1, A2, Def10; :: thesis: verum

end;

suppose ( born (R,x) <> A & born (R,y) <> A ) ; :: thesis: [x,y] in ClosedProd (R,A,A)

then ( born (R,x) in A & born (R,y) in A ) by ORDINAL1:11, A2, XBOOLE_0:def 8;
hence [x,y] in ClosedProd (R,A,A) by A1, Def10; :: thesis: verum

end;

end;