let I be set ; :: thesis: ( not I is empty implies for X being ManySortedSet of I holds
( not X is V3() or not X is V2() ) )
assume A1: not I is empty ; :: thesis: for X being ManySortedSet of I holds
( not X is V3() or not X is V2() )
given X being ManySortedSet of I such that A2: X is V3() and
A3: X is V2() ; :: thesis: contradiction
consider i being object such that
A4: i in I by A1, XBOOLE_0:def 1;
X . i is empty by A2, A4;
hence contradiction by A3, A4; :: thesis: verum