let A, B be Ordinal; :: thesis: for R being Relation
for a, b being object holds
( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) iff ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) )
let R be Relation; :: thesis: for a, b being object holds
( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) iff ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) )
let a, b be object ; :: thesis: ( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) iff ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) )
thus ( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) implies ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) ) :: thesis: ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) implies [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) )

proof

assume A1: [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) ; :: thesis: ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) )
then A2: ( [a,b] in ClosedProd (R,A,B) & not [a,b] in OpenProd (R,A,B) ) by XBOOLE_0:def 5;
A3: ( a in Day (R,A) & b in Day (R,A) ) by ZFMISC_1:87, A1;

per cases then ( ( born (R,a) in A & born (R,b) in A ) or ( born (R,a) = A & born (R,b) c= B ) or ( born (R,a) c= B & born (R,b) = A ) ) by A2, Def10;

suppose ( born (R,a) in A & born (R,b) in A ) ; :: thesis: ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) )

hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A2, A3, Def9; :: thesis: verum

end;

suppose A4: ( born (R,a) = A & born (R,b) c= B ) ; :: thesis: ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) )

then not born (R,b) in B by A2, A3, Def9;
then B c= born (R,b) by ORDINAL1:16;
hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A1, ZFMISC_1:87, A4, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A5: ( born (R,a) c= B & born (R,b) = A ) ; :: thesis: ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) )

then not born (R,a) in B by A2, A3, Def9;
then B c= born (R,a) by ORDINAL1:16;
hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A1, ZFMISC_1:87, A5, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

assume that
A6: ( a in Day (R,A) & b in Day (R,A) ) and
A7: ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ; :: thesis: [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B))
A8: not [a,b] in OpenProd (R,A,B)

proof

assume [a,b] in OpenProd (R,A,B) ; :: thesis: contradiction
then ( ( born (R,a) in A & born (R,b) in A ) or ( born (R,a) = A & born (R,b) in B ) or ( born (R,a) in B & born (R,b) = A ) ) by A6, Def9;
hence contradiction by A7; :: thesis: verum

end;

[a,b] in ClosedProd (R,A,B) by A6, A7, Def10;
hence [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 5; :: thesis: verum