let i be object ; :: according to PBOOLE:def 12 :: thesis: ( not i in I or (MSUnion A) . i is empty )

set MA = MSUnion A;

assume i in I ; :: thesis: (MSUnion A) . i is empty

then A1: (MSUnion A) . i = union { (f . i) where f is Element of Bool M : f in A } by Def2;

assume not (MSUnion A) . i is empty ; :: thesis: contradiction

then consider v being object such that

A2: v in (MSUnion A) . i ;

consider h being set such that

v in h and

A3: h in { (f . i) where f is Element of Bool M : f in A } by A1, A2, TARSKI:def 4;

ex g being Element of Bool M st

( h = g . i & g in A ) by A3;

hence contradiction ; :: thesis: verum

set MA = MSUnion A;

assume i in I ; :: thesis: (MSUnion A) . i is empty

then A1: (MSUnion A) . i = union { (f . i) where f is Element of Bool M : f in A } by Def2;

assume not (MSUnion A) . i is empty ; :: thesis: contradiction

then consider v being object such that

A2: v in (MSUnion A) . i ;

consider h being set such that

v in h and

A3: h in { (f . i) where f is Element of Bool M : f in A } by A1, A2, TARSKI:def 4;

ex g being Element of Bool M st

( h = g . i & g in A ) by A3;

hence contradiction ; :: thesis: verum