let x be Surreal; :: thesis: for X, Y being set
for Inv being Function st Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued holds
divset (Y,x,X,Inv) is surreal-membered
let X, Y be set ; :: thesis: for Inv being Function st Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued holds
divset (Y,x,X,Inv) is surreal-membered
let Inv be Function; :: thesis: ( Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued implies divset (Y,x,X,Inv) is surreal-membered )
assume A1: ( Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued ) ; :: thesis: divset (Y,x,X,Inv) is surreal-membered
let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in divset (Y,x,X,Inv) or o is surreal )
assume o in divset (Y,x,X,Inv) ; :: thesis: o is surreal
then consider l being object such that
A2: ( l in Y & o in divs (l,x,X,Inv) ) by Def3;
reconsider l = l as Surreal by A1, A2;
divs (l,x,X,Inv) is surreal-membered by Th4;
hence o is surreal by A2; :: thesis: verum