let x be Surreal; :: thesis: for X, Y, Z being set
for Inv being Function st Y c= Z holds
divset (Y,x,X,Inv) c= divset (Z,x,X,Inv)
let X, Y, Z be set ; :: thesis: for Inv being Function st Y c= Z holds
divset (Y,x,X,Inv) c= divset (Z,x,X,Inv)
let Inv be Function; :: thesis: ( Y c= Z implies divset (Y,x,X,Inv) c= divset (Z,x,X,Inv) )
assume A1: Y c= Z ; :: thesis: divset (Y,x,X,Inv) c= divset (Z,x,X,Inv)
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset (Y,x,X,Inv) or o in divset (Z,x,X,Inv) )
assume o in divset (Y,x,X,Inv) ; :: thesis: o in divset (Z,x,X,Inv)
then ex lamb being object st
( lamb in Y & o in divs (lamb,x,X,Inv) ) by Def3;
hence o in divset (Z,x,X,Inv) by A1, Def3; :: thesis: verum