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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (support (SMoebius X)) \/ (support (SMoebius Y)) or x in support ((SMoebius X) + (SMoebius Y)) )
( 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: x in support ((SMoebius X) + (SMoebius Y))

per cases ( x in support (SMoebius X) or x in support (SMoebius Y) ) by A3, XBOOLE_0:def 3;

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

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: verum

end;

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

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: verum

end;

end;

end;

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