let I be set ; :: thesis: for x, y, X being ManySortedSet of st not I is empty holds
{x,y} \/ X <> [0] I
let x, y, X be ManySortedSet of ; :: thesis: ( not I is empty implies {x,y} \/ X <> [0] I )
assume that
A1: not I is empty and
A2: {x,y} \/ X = [0] I ; :: thesis: contradiction
consider i being set 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 7;
hence contradiction by A2, PBOOLE:5; :: thesis: verum