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