let I be set ; :: thesis: for X, A being ManySortedSet of holds
( X c= A iff X in bool A )
let X, A be ManySortedSet of ; :: thesis: ( X c= A iff X in bool A )
thus ( X c= A implies X in bool A ) :: thesis: ( X in bool A implies X c= A )

proof

assume A1: X c= A ; :: thesis: X in bool A
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or X . i in (bool A) . i )
assume A2: i in I ; :: thesis: X . i in (bool A) . i
then X . i c= A . i by A1, PBOOLE:def 5;
then X . i in bool (A . i) ;
hence X . i in (bool A) . i by A2, Def1; :: thesis: verum

end;

assume A3: X in bool A ; :: thesis: X c= A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or X . i c= A . i )
assume A4: i in I ; :: thesis: X . i c= A . i
then X . i in (bool A) . i by A3, PBOOLE:def 4;
then X . i in bool (A . i) by A4, Def1;
hence X . i c= A . i ; :: thesis: verum