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 Lm3; :: thesis: verum