let x be Surreal; :: thesis: for X, Y being set
for Inv being Function holds divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)
let X, Y be set ; :: thesis: for Inv being Function holds divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)
let Inv be Function; :: thesis: divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)
thus divset (Y,x,X,Inv) c= divset (Y,x,(X \ {0_No}),Inv) :: according to XBOOLE_0:def 10 :: thesis: divset (Y,x,(X \ {0_No}),Inv) c= divset (Y,x,X,Inv)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset (Y,x,X,Inv) or o in divset (Y,x,(X \ {0_No}),Inv) )
assume o in divset (Y,x,X,Inv) ; :: thesis: o in divset (Y,x,(X \ {0_No}),Inv)
then consider lamb being object such that
A1: ( lamb in Y & o in divs (lamb,x,X,Inv) ) by Def3;
o in divs (lamb,x,(X \ {0_No}),Inv) by A1, Th7;
hence o in divset (Y,x,(X \ {0_No}),Inv) by A1, Def3; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset (Y,x,(X \ {0_No}),Inv) or o in divset (Y,x,X,Inv) )
assume o in divset (Y,x,(X \ {0_No}),Inv) ; :: thesis: o in divset (Y,x,X,Inv)
then consider lamb being object such that
A2: ( lamb in Y & o in divs (lamb,x,(X \ {0_No}),Inv) ) by Def3;
o in divs (lamb,x,X,Inv) by A2, Th7;
hence o in divset (Y,x,X,Inv) by A2, Def3; :: thesis: verum