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

proof

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

proof

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

end;

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

end;

assume A4: ( X c= A & X misses 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 A5: i in I ; :: thesis: X . i c= (A (\) B) . i
then ( X . i c= A . i & X . i misses B . i ) by A4;
then X . i c= (A . i) \ (B . i) by XBOOLE_1:86;
hence X . i c= (A (\) B) . i by A5, PBOOLE:def 6; :: thesis: verum