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

proof

assume A1: {x} \ X = [0] I ; :: thesis: x in X
let i be set ; :: according to PBOOLE:def 4 :: 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 9
.= {} by A1, PBOOLE:5 ;
hence x . i in X . i by ZFMISC_1:68; :: thesis: verum

end;

assume A3: x in X ; :: thesis: {x} \ X = [0] I

now

let i be set ; :: thesis: ( i in I implies ({x} \ X) . i = ([0] I) . i )
assume A4: i in I ; :: thesis: ({x} \ X) . i = ([0] I) . i
then A5: x . i in X . i by A3, PBOOLE:def 4;
thus ({x} \ X) . i = ({x} . i) \ (X . i) by A4, PBOOLE:def 9
.= {(x . i)} \ (X . i) by A4, Def1
.= {} by A5, ZFMISC_1:68
.= ([0] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence {x} \ X = [0] I by PBOOLE:3; :: thesis: verum