let I be set ; :: thesis: for x, y being ManySortedSet of I st not I is empty & {x} (/\) {y} = EmptyMS I holds
x <> y
let x, y be ManySortedSet of I; :: thesis: ( not I is empty & {x} (/\) {y} = EmptyMS I implies x <> y )
assume that
A1: not I is empty and
A2: {x} (/\) {y} = EmptyMS I ; :: thesis: x <> y
now :: thesis: ex i being object st x . i <> y . i
consider i being object such that
A3: i in I by A1, XBOOLE_0:def 1;
take i = i; :: thesis: x . i <> y . i
{(x . i)} /\ {(y . i)} = ({x} . i) /\ {(y . i)} by A3, Def1
.= ({x} . i) /\ ({y} . i) by A3, Def1
.= ({x} (/\) {y}) . i by A3, PBOOLE:def 5
.= {} by A2, PBOOLE:5 ;
hence x . i <> y . i ; :: thesis: verum
end;
hence x <> y ; :: thesis: verum