let I be set ; :: thesis: for A, X being ManySortedSet of I holds
( X c= A iff X in bool A )
let A, X be ManySortedSet of I; :: 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 object ; :: according to PBOOLE:def 1 :: 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;
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 object ; :: according to PBOOLE:def 2 :: 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;
then X . i in bool (A . i) by A4, Def1;
hence X . i c= A . i ; :: thesis: verum