let I be set ; :: thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} (/\) X = EmptyMS I holds
( not x in X & not y in X )
let x, y, X be ManySortedSet of I; :: thesis: ( not I is empty & {x,y} (/\) X = EmptyMS I implies ( not x in X & not y in X ) )
assume that
A1: not I is empty and
A2: {x,y} (/\) X = EmptyMS I ; :: thesis: ( not x in X & not y in X )

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

let i be object ; :: thesis: ( i in I implies {(x . i),(y . i)} /\ (X . i) = {} )
assume A4: i in I ; :: thesis: {(x . i),(y . i)} /\ (X . i) = {}
hence {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2
.= ({x,y} (/\) X) . i by A4, PBOOLE:def 5
.= {} by A2, PBOOLE:5 ;
:: thesis: verum

end;

thus not x in X :: thesis: not y in X

proof

assume A5: x in X ; :: thesis: contradiction

now :: thesis: ex i being object st
( i in I & not x . i in X . i )

consider i being object such that
A6: i in I by A1, XBOOLE_0:def 1;
take i = i; :: thesis: ( i in I & not x . i in X . i )
{(x . i),(y . i)} /\ (X . i) = {} by A3, A6;
then {(x . i),(y . i)} misses X . i by XBOOLE_0:def 7;
hence ( i in I & not x . i in X . i ) by A6, ZFMISC_1:49; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

assume A7: y in X ; :: thesis: contradiction

now :: thesis: ex i being object st
( i in I & not y . i in X . i )

consider i being object such that
A8: i in I by A1, XBOOLE_0:def 1;
take i = i; :: thesis: ( i in I & not y . i in X . i )
{(x . i),(y . i)} /\ (X . i) = {} by A3, A8;
then {(x . i),(y . i)} misses X . i by XBOOLE_0:def 7;
hence ( i in I & not y . i in X . i ) by A8, ZFMISC_1:49; :: thesis: verum

end;

hence contradiction by A7; :: thesis: verum