let X be set ; :: thesis: for x, y being Surreal st X << {x} & x <= y holds
X << {y}
let x, y be Surreal; :: thesis: ( X << {x} & x <= y implies X << {y} )
assume A1: ( X << {x} & x <= y ) ; :: thesis: X << {y}
let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in X or not b₁ in {y} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in X or not r in {y} or not l >= r )
assume A2: ( l in X & r in {y} ) ; :: thesis: not l >= r
x in {x} by TARSKI:def 1;
then l < y by A1, Th4, A2;
hence not l >= r by A2, TARSKI:def 1; :: thesis: verum