let X be set ; :: thesis: for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2)
let b1, b2 be real-valued ManySortedSet of X; :: thesis: support (b1 + b2) c= (support b1) \/ (support b2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (b1 + b2) or x in (support b1) \/ (support b2) )
assume x in support (b1 + b2) ; :: thesis: x in (support b1) \/ (support b2)
then A1: (b1 + b2) . x <> 0 by Def7;
assume A2: not x in (support b1) \/ (support b2) ; :: thesis: contradiction
then not x in support b1 by XBOOLE_0:def 3;
then A3: b1 . x = 0 by Def7;
not x in support b2 by A2, XBOOLE_0:def 3;
then (b1 . x) + (b2 . x) = 0 by A3, Def7;
hence contradiction by A1, Def5; :: thesis: verum