let X, Y be surreal-membered set ; :: thesis: ( X <<= Y iff -- Y <<= -- X )
( -- (-- X) = X & -- (-- Y) = Y ) by Th15;
hence ( X <<= Y iff -- Y <<= -- X ) by Lm2; :: thesis: verum