:: deftheorem Def10 defines ClosedProd SURREAL0:def 10 :
for R being Relation
for A, B being Ordinal
for b₄ being Relation of (Day (R,A)) holds
( b₄ = ClosedProd (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) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) ) );