let i be set ; :: according to PBOOLE:def 15 :: 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 Def4;
assume not (MSUnion A) . i is empty ; :: thesis: contradiction
then consider v being set such that
A2: v in (MSUnion A) . i by XBOOLE_0:def 1;
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