let I be set ; :: thesis: for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
let X, A, B 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 set ; :: 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, PBOOLE:def 1;
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 set ; :: 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, PBOOLE:def 1;
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 set ; :: 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, PBOOLE:def 8;
then A7: X . i misses (A . i) /\ (B . i) by A6, PBOOLE:def 5;
X . i c= (A \/ B) . i by A4, A6, PBOOLE:def 2;
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