:: deftheorem Def9 defines OpenProd SURREAL0:def 9 :
for R being Relation
for A, B being Ordinal
for b₄ being Relation of (Day (R,A)) holds
( b₄ = OpenProd (R,A,B) iff for x, y being Element of Day (R,A) holds
( [x,y] in b₄ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) );