let o be object ; :: thesis: for X, Y, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divset (Y,o,X,I1) = divset (Y,o,X,I2)
let X, Y, Z be set ; :: thesis: for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divset (Y,o,X,I1) = divset (Y,o,X,I2)
let I1, I2 be Function; :: thesis: ( X \ {0_No} c= Z & I1 | Z = I2 | Z implies divset (Y,o,X,I1) = divset (Y,o,X,I2) )
assume A1: ( X \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis: divset (Y,o,X,I1) = divset (Y,o,X,I2)
thus divset (Y,o,X,I1) c= divset (Y,o,X,I2) :: according to XBOOLE_0:def 10 :: thesis: divset (Y,o,X,I2) c= divset (Y,o,X,I1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in divset (Y,o,X,I1) or a in divset (Y,o,X,I2) )
assume a in divset (Y,o,X,I1) ; :: thesis: a in divset (Y,o,X,I2)
then consider lamb being object such that
A2: ( lamb in Y & a in divs (lamb,o,X,I1) ) by Def3;
divs (lamb,o,X,I1) = divs (lamb,o,X,I2) by A1, Th14;
hence a in divset (Y,o,X,I2) by A2, Def3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in divset (Y,o,X,I2) or a in divset (Y,o,X,I1) )
assume a in divset (Y,o,X,I2) ; :: thesis: a in divset (Y,o,X,I1)
then consider lamb being object such that
A3: ( lamb in Y & a in divs (lamb,o,X,I2) ) by Def3;
divs (lamb,o,X,I1) = divs (lamb,o,X,I2) by A1, Th14;
hence a in divset (Y,o,X,I1) by A3, Def3; :: thesis: verum