let i be object ; PBOOLE:def 12 ( not i in I or (MSUnion A) . i is empty )
set MA = MSUnion A;
assume
i in I
; (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
; 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
; verum