theorem Th33: :: SURREAL0:33

for A being Ordinal
for a, b being object holds
( [a,b] in ClosedProd ((No_Ord A),A,A) iff ( a in Day A & b in Day A ) )