theorem Th32: :: SURREAL0:32

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