let I be set ; :: thesis: for x, X, Y being ManySortedSet of I st x in X (\) Y holds
x in X
let x, X, Y be ManySortedSet of I; :: thesis: ( x in X (\) Y implies x in X )
assume A1: x in X (\) Y ; :: thesis: x in X
thus x in X :: thesis: verum

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in X . i )
assume A2: i in I ; :: thesis: x . i in X . i
then x . i in (X (\) Y) . i by A1;
then x . i in (X . i) \ (Y . i) by A2, Def6;
hence x . i in X . i ; :: thesis: verum

end;