theorem Th16: :: SURREAL0:16

for A, B being Ordinal
for R being Relation holds OpenProd (R,A,B) c= ClosedProd (R,A,B)