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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in support (b1 -' b2) ; :: thesis:
assume not x in support b1 ; :: thesis:
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:

end;