set DU = { (union P) where P is Subset of D : verum } ;
now :: thesis: for a, b being set st a in { (union P) where P is Subset of D : verum } & b in { (union P) where P is Subset of D : verum } holds
a /\ b in { (union P) where P is Subset of D : verum }
let a, b be set ; :: thesis: ( a in { (union P) where P is Subset of D : verum } & b in { (union P) where P is Subset of D : verum } implies a /\ b in { (union P) where P is Subset of D : verum } )
assume that
A1: a in { (union P) where P is Subset of D : verum } and
A2: b in { (union P) where P is Subset of D : verum } ; :: thesis: a /\ b in { (union P) where P is Subset of D : verum }
consider Pa being Subset of D such that
A3: a = union Pa by A1;
consider Pb being Subset of D such that
A4: b = union Pb by A2;
now :: thesis: for X, Y being set st X <> Y & X in Pa \/ Pb & Y in Pa \/ Pb holds
X misses Y
let X, Y be set ; :: thesis: ( X <> Y & X in Pa \/ Pb & Y in Pa \/ Pb implies X misses Y )
assume that
A5: X <> Y and
A6: X in Pa \/ Pb and
A7: Y in Pa \/ Pb ; :: thesis: X misses Y
( X in D & Y in D ) by A6, A7;
hence X misses Y by A5, EQREL_1:def 4; :: thesis: verum
end;
then (union Pa) /\ (union Pb) = union (Pa /\ Pb) by ZFMISC_1:83;
hence a /\ b in { (union P) where P is Subset of D : verum } by A3, A4; :: thesis: verum
end;
then { (union P) where P is Subset of D : verum } is cap-closed ;
hence UniCl D is intersection_stable by Th14; :: thesis: verum