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

proof

assume A1: {x,y} (\) X = EmptyMS I ; :: thesis: ( x in X & y in X )
thus x in X :: thesis: y in X

proof

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),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2
.= ({x,y} (\) X) . i by A2, PBOOLE:def 6
.= {} by A1, PBOOLE:5 ;
hence x . i in X . i by ZFMISC_1:64; :: thesis: verum

end;

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or y . i in X . i )
assume A3: i in I ; :: thesis: y . i in X . i
then {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2
.= ({x,y} (\) X) . i by A3, PBOOLE:def 6
.= {} by A1, PBOOLE:5 ;
hence y . i in X . i by ZFMISC_1:64; :: thesis: verum

end;

assume that
A4: x in X and
A5: y in X ; :: thesis: {x,y} (\) X = EmptyMS I

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

let i be object ; :: thesis: ( i in I implies ({x,y} (\) X) . i = (EmptyMS I) . i )
assume A6: i in I ; :: thesis: ({x,y} (\) X) . i = (EmptyMS I) . i
then A7: x . i in X . i by A4;
A8: y . i in X . i by A5, A6;
thus ({x,y} (\) X) . i = ({x,y} . i) \ (X . i) by A6, PBOOLE:def 6
.= {(x . i),(y . i)} \ (X . i) by A6, Def2
.= {} by A7, A8, ZFMISC_1:64
.= (EmptyMS I) . i by PBOOLE:5 ; :: thesis: verum

end;

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