let I, J be set ; :: thesis: for m being bag of I holds support (m -' (m | J)) = (support m) \ J
let m be bag of I; :: thesis: support (m -' (m | J)) = (support m) \ J
thus support (m -' (m | J)) c= (support m) \ J :: according to XBOOLE_0:def 10 :: thesis: (support m) \ J c= support (m -' (m | J))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (m -' (m | J)) or x in (support m) \ J )
assume x in support (m -' (m | J)) ; :: thesis: x in (support m) \ J
then (m -' (m | J)) . x <> 0 by PRE_POLY:def 7;
then (m . x) -' ((m | J) . x) <> 0 by PRE_POLY:def 6;
then (m . x) -' ((m | J) . x) > 0 ;
then (m . x) - ((m | J) . x) > 0 by XREAL_0:def 2;
then m . x > (m | J) . x by XREAL_1:47;
then ( m . x <> (m | J) . x & x in dom m & dom m = I & m . x > 0 ) by PARTFUN1:def 2, FUNCT_1:def 2;
then ( not x in J & x in support m ) by BAR, PRE_POLY:def 7;
hence x in (support m) \ J by XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (support m) \ J or x in support (m -' (m | J)) )
assume x in (support m) \ J ; :: thesis: x in support (m -' (m | J))
then A1: ( x in support m & not x in J ) by XBOOLE_0:def 5;
then A2: m . x <> 0 by PRE_POLY:def 7;
then ( x in dom m & dom m = I ) by PARTFUN1:def 2, FUNCT_1:def 2;
then (m | J) . x = 0 by A1, BAR;
then ( (m -' (m | J)) . x = (m . x) -' ((m | J) . x) & (m . x) -' ((m | J) . x) <> 0 ) by A2, NAT_D:40, PRE_POLY:def 6;
hence x in support (m -' (m | J)) by PRE_POLY:def 7; :: thesis: verum