theorem Th25: :: SURREAL0:25

for A, B being Ordinal
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 ) ) ) )