let I be set ; :: thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} /\ X = [0] 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 = [0] I implies ( not x in X & not y in X ) )
assume that
A1: not I is empty and
A2: {x,y} /\ X = [0] I ; :: thesis: ( not x in X & not y in X )

A3: now

let i be set ; :: 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 8
.= {} 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

consider i being set 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:55; :: thesis: verum

end;

hence contradiction by A5, PBOOLE:def 4; :: thesis: verum

end;

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

now

consider i being set 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:55; :: thesis: verum

end;

hence contradiction by A7, PBOOLE:def 4; :: thesis: verum