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 set such that
A4: i in I by A1, XBOOLE_0:def 1;
( X . i is empty & not X . i is empty ) by A2, A3, A4, PBOOLE:def 15, PBOOLE:def 16;
hence contradiction ; :: thesis: verum