let X, Y be finite Subset of NAT; :: thesis:
assume A1: X misses Y ; :: thesis:
thus (support (SMoebius X)) \/ (support (SMoebius Y)) c= support ((SMoebius X) + (SMoebius Y)) :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
( support (SMoebius X) = X /\ SCNAT & support (SMoebius Y) = Y /\ SCNAT ) by Def5;
then A2: support (SMoebius X) misses support (SMoebius Y) by A1, XBOOLE_1:76;
assume A3: x in (support (SMoebius X)) \/ (support (SMoebius Y)) ; :: thesis:

per cases by A3, XBOOLE_0:def 3;

suppose A4: x in support (SMoebius X) ; :: thesis:

then not x in support (SMoebius Y) by A2, XBOOLE_0:3;
then (SMoebius Y) . x = 0 by PRE_POLY:def 7;
then ((SMoebius X) . x) + ((SMoebius Y) . x) <> 0 by A4, PRE_POLY:def 7;
then ((SMoebius X) + (SMoebius Y)) . x <> 0 by PRE_POLY:def 5;
hence x in support ((SMoebius X) + (SMoebius Y)) by PRE_POLY:def 7; :: thesis:

end;

suppose A5: x in support (SMoebius Y) ; :: thesis:

then not x in support (SMoebius X) by A2, XBOOLE_0:3;
then (SMoebius X) . x = 0 by PRE_POLY:def 7;
then ((SMoebius X) . x) + ((SMoebius Y) . x) <> 0 by A5, PRE_POLY:def 7;
then ((SMoebius X) + (SMoebius Y)) . x <> 0 by PRE_POLY:def 5;
hence x in support ((SMoebius X) + (SMoebius Y)) by PRE_POLY:def 7; :: thesis:

end;

end;

end;

thus support ((SMoebius X) + (SMoebius Y)) c= (support (SMoebius X)) \/ (support (SMoebius Y)) by PRE_POLY:75; :: thesis: