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

proof

set A = Int (Cl (union F));
Int (Cl (union F)) is open_condensed by A1, Th83;
then Int (Cl (union F)) in { C where C is Subset of T : C is open_condensed } ;
then A3: Int (Cl (union F)) in Open_Domains_of T by TDLAT_1:def 9;
then reconsider a = Int (Cl (union F)) as Element of (Open_Domains_Lattice T) by Th103;
A4: X is_less_than a

proof

let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def 17 :: thesis: ( not b in X or b [= a )
reconsider B = b as Element of Open_Domains_of T by Th103;
assume A5: b in X ; :: thesis: b [= a
F is open by A1, Th81;
then B c= Int (Cl (union F)) by A2, A5, Th84;
hence b [= a by A3, Th106; :: thesis: verum

end;

A6: for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds
a [= b

proof

let b be Element of (Open_Domains_Lattice T); :: thesis: ( X is_less_than b implies a [= b )
reconsider B = b as Element of Open_Domains_of T by Th103;
B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def 9;
then A7: ex C being Subset of T st
( C = B & C is open_condensed ) ;
assume A8: X is_less_than b ; :: thesis: a [= b
for C being Subset of T st C in F holds
C c= B

proof

let C be Subset of T; :: thesis: ( C in F implies C c= B )
reconsider C1 = C as Subset of T ;
assume A9: C in F ; :: thesis: C c= B
then C1 is open_condensed by A1, Def4;
then C in { P where P is Subset of T : P is open_condensed } ;
then A10: C in Open_Domains_of T by TDLAT_1:def 9;
then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103;
c [= b by A2, A8, A9, LATTICE3:def 17;
hence C c= B by A10, Th106; :: thesis: verum

end;

then Int (Cl (union F)) c= B by A7, Th84;
hence a [= b by A3, Th106; :: thesis: verum

end;

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

end;