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

now

consider i being set 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 8
.= {} by A2, PBOOLE:5 ;
hence x . i <> y . i ; :: thesis: verum

end;

hence x <> y ; :: thesis: verum