theorem Th30: :: SURREAL0:30

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