let x, y be Surreal; :: thesis: for X being set
for Inv being Function holds divs (y,x,X,Inv) is surreal-membered
let X be set ; :: thesis: for Inv being Function holds divs (y,x,X,Inv) is surreal-membered
let Inv be Function; :: thesis: divs (y,x,X,Inv) is surreal-membered
let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in divs (y,x,X,Inv) or o is surreal )
assume o in divs (y,x,X,Inv) ; :: thesis: o is surreal
then ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' y)) *' (Inv . xL) ) by Def2;
hence o is surreal ; :: thesis: verum