let X be set ; :: thesis: for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1
let b1, b2 be natural-valued ManySortedSet of X; :: thesis: support (b1 -' b2) c= support b1
thus support (b1 -' b2) c= support b1 :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (b1 -' b2) or x in support b1 )
assume A1: x in support (b1 -' b2) ; :: thesis: x in support b1
assume not x in support b1 ; :: thesis: contradiction
then b1 . x = 0 by Def7;
then (b1 . x) -' (b2 . x) = 0 by NAT_2:8;
then (b1 -' b2) . x = 0 by Def6;
hence contradiction by A1, Def7; :: thesis: verum

end;