let I be set ; :: thesis: for x, X being ManySortedSet of I st not I is empty & {x} (/\) X = EmptyMS I holds
not x in X
let x, X be ManySortedSet of I; :: thesis: ( not I is empty & {x} (/\) X = EmptyMS I implies not x in X )
assume that
A1: not I is empty and
A2: {x} (/\) X = EmptyMS I and
A3: x in X ; :: thesis: contradiction
consider i being object such that
A4: i in I by A1, XBOOLE_0:def 1;
{(x . i)} /\ (X . i) = ({x} . i) /\ (X . i) by A4, Def1
.= ({x} (/\) X) . i by A4, PBOOLE:def 5
.= {} by A2, PBOOLE:5 ;
then {(x . i)} misses X . i by XBOOLE_0:def 7;
then not x . i in X . i by ZFMISC_1:48;
hence contradiction by A3, A4; :: thesis: verum