let I be set ; :: thesis: for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
let X, A, B 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 set ; :: according to PBOOLE:def 5 :: 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, PBOOLE:def 4;
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 set ; :: according to PBOOLE:def 11 :: 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, PBOOLE:def 4;
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 set ; :: according to PBOOLE:def 5 :: 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, PBOOLE:def 5, PBOOLE:def 11;
then X . i c= (A . i) \ (B . i) by XBOOLE_1:86;
hence X . i c= (A \ B) . i by A5, PBOOLE:def 9; :: thesis: verum