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

proof

assume A1: {x} c= X ; :: thesis: x in X
let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in X . i )
assume A2: i in I ; :: thesis: x . i in X . i
then {x} . i c= X . i by A1, PBOOLE:def 2;
then {(x . i)} c= X . i by A2, Def1;
hence x . i in X . i by ZFMISC_1:31; :: thesis: verum

end;

assume A3: x in X ; :: thesis: {x} c= X
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or {x} . i c= X . i )
assume A4: i in I ; :: thesis: {x} . i c= X . i
then x . i in X . i by A3, PBOOLE:def 1;
then {(x . i)} c= X . i by ZFMISC_1:31;
hence {x} . i c= X . i by A4, Def1; :: thesis: verum