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

proof

assume A1: {x} (\) X = EmptyMS I ; :: thesis: x in X
let i be object ; :: 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)} \ (X . i) = ({x} . i) \ (X . i) by Def1
.= ({x} (\) X) . i by A2, PBOOLE:def 6
.= {} by A1, PBOOLE:5 ;
hence x . i in X . i by ZFMISC_1:60; :: thesis: verum

end;

assume A3: x in X ; :: thesis: {x} (\) X = EmptyMS I

now :: thesis: for i being object st i in I holds
({x} (\) X) . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies ({x} (\) X) . i = (EmptyMS I) . i )
assume A4: i in I ; :: thesis: ({x} (\) X) . i = (EmptyMS I) . i
then A5: x . i in X . i by A3;
thus ({x} (\) X) . i = ({x} . i) \ (X . i) by A4, PBOOLE:def 6
.= {(x . i)} \ (X . i) by A4, Def1
.= {} by A5, ZFMISC_1:60
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence {x} (\) X = EmptyMS I ; :: thesis: verum