let I be set ; :: thesis: for A, B, X being ManySortedSet of I holds
( X c= A (\+\) B iff ( X c= A (\/) B & X misses A (/\) B ) )
let A, B, X be ManySortedSet of I; :: thesis: ( X c= A (\+\) B iff ( X c= A (\/) B & X misses A (/\) B ) )
thus ( X c= A (\+\) B implies ( X c= A (\/) B & X misses A (/\) B ) ) :: thesis: ( X c= A (\/) B & X misses A (/\) B implies X c= A (\+\) B )

proof

assume X c= A (\+\) B ; :: thesis: ( X c= A (\/) B & X misses A (/\) B )
then A1: X in bool (A (\+\) B) by Th1;
thus X c= A (\/) B :: thesis: X misses A (/\) B

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= (A (\/) B) . i )
assume A2: i in I ; :: thesis: X . i c= (A (\/) B) . i
then X . i in (bool (A (\+\) B)) . i by A1;
then X . i in bool ((A . i) \+\ (B . i)) by A2, Lm5;
then X . i c= (A . i) \/ (B . i) by XBOOLE_1:107;
hence X . i c= (A (\/) B) . i by A2, PBOOLE:def 4; :: thesis: verum

end;

let i be object ; :: according to PBOOLE:def 8 :: thesis: ( not i in I or X . i misses (A (/\) B) . i )
assume A3: i in I ; :: thesis: X . i misses (A (/\) B) . i
then X . i in (bool (A (\+\) B)) . i by A1;
then X . i in bool ((A . i) \+\ (B . i)) by A3, Lm5;
then X . i misses (A . i) /\ (B . i) by XBOOLE_1:107;
hence X . i misses (A (/\) B) . i by A3, PBOOLE:def 5; :: thesis: verum

end;

assume that
A4: X c= A (\/) B and
A5: X misses A (/\) B ; :: thesis: X c= A (\+\) B
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= (A (\+\) B) . i )
assume A6: i in I ; :: thesis: X . i c= (A (\+\) B) . i
then X . i misses (A (/\) B) . i by A5;
then A7: X . i misses (A . i) /\ (B . i) by A6, PBOOLE:def 5;
X . i c= (A (\/) B) . i by A4, A6;
then X . i c= (A . i) \/ (B . i) by A6, PBOOLE:def 4;
then X . i c= (A . i) \+\ (B . i) by A7, XBOOLE_1:107;
hence X . i c= (A (\+\) B) . i by A6, PBOOLE:4; :: thesis: verum