let I be set ; :: thesis: ( not I is empty implies for X being ManySortedSet of I holds
( not X is empty-yielding or not X is non-empty ) )
assume A1: not I is empty ; :: thesis: for X being ManySortedSet of I holds
( not X is empty-yielding or not X is non-empty )
given X being ManySortedSet of I such that A2: X is empty-yielding and
A3: X is non-empty ; :: 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