let T be non empty TopSpace; :: thesis: for F being Subset-Family of st F is domains-family holds
for X being Subset of st X = F holds
"\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F)))
let F be Subset-Family of ; :: thesis: ( F is domains-family implies for X being Subset of st X = F holds
"\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F))) )
assume A1: F is domains-family ; :: thesis: for X being Subset of st X = F holds
"\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F)))
let X be Subset of ; :: thesis: ( X = F implies "\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F))) )
assume A2: X = F ; :: thesis: "\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F)))
thus "\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F))) :: thesis: verum

proof

set A = (union F) \/ (Int (Cl (union F)));
(union F) \/ (Int (Cl (union F))) is condensed by A1, Th68;
then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of : C is condensed } ;
then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def 1;
then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of by Th86;
A4: X is_less_than a

proof

let b be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not b in X or b [= a )
reconsider B = b as Element of Domains_of T by Th86;
assume b in X ; :: thesis: b [= a
then B c= (union F) \/ (Int (Cl (union F))) by A2, Th69;
hence b [= a by A3, Th89; :: thesis: verum

end;

A5: for b being Element of st X is_less_than b holds
a [= b

proof

let b be Element of ; :: thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Domains_of T by Th86;
assume A6: X is_less_than b ; :: thesis: a [= b
A7: for C being Subset of st C in F holds
C c= B

proof

let C be Subset of ; :: thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of ;
assume A8: C in F ; :: thesis: C c= B
then C1 is condensed by A1, Def2;
then C in { P where P is Subset of : P is condensed } ;
then A9: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of by Th86;
c [= b by A2, A6, A8, LATTICE3:def 17;
hence C c= B by A9, Th89; :: thesis: verum

end;

B in Domains_of T ;
then B in { C where C is Subset of : C is condensed } by TDLAT_1:def 1;
then ex C being Subset of st
( C = B & C is condensed ) ;
then (union F) \/ (Int (Cl (union F))) c= B by A7, Th69;
hence a [= b by A3, Th89; :: thesis: verum

end;

Domains_Lattice T is complete by Th91;
hence "\/" X,(Domains_Lattice T) = (union F) \/ (Int (Cl (union F))) by A4, A5, LATTICE3:def 21; :: thesis: verum

end;