let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) & ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) )
let F be Subset-Family of T; :: thesis: ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) & ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) ) )
assume A1: F is closed-domains-family ; :: thesis: for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) & ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) )
let X be Subset of (Closed_Domains_Lattice T); :: thesis: ( X = F implies ( ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) & ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) ) )
assume A2: X = F ; :: thesis: ( ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) & ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) )
thus ( X <> {} implies "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) ) :: thesis: ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T )

proof

assume A3: X <> {} ; :: thesis: "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F))
set A = Cl (Int (meet F));
Cl (Int (meet F)) is closed_condensed by A1, Th76;
then Cl (Int (meet F)) in { C where C is Subset of T : C is closed_condensed } ;
then A4: Cl (Int (meet F)) in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = Cl (Int (meet F)) as Element of (Closed_Domains_Lattice T) by Th94;
A5: a is_less_than X

proof

let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def 16 :: thesis: ( not b in X or a [= b )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume A6: b in X ; :: thesis: a [= b
F is closed by A1, Th74;
then Cl (Int (meet F)) c= B by A2, A6, Th78;
hence a [= b by A4, Th97; :: thesis: verum

end;

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

proof

let b be Element of (Closed_Domains_Lattice T); :: thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
B in Closed_Domains_of T ;
then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def 5;
then A8: ex C being Subset of T st
( C = B & C is closed_condensed ) ;
assume A9: b is_less_than X ; :: thesis: b [= a
for C being Subset of T st C in F holds
B c= C

proof

let C be Subset of T; :: thesis: ( C in F implies B c= C )
reconsider C1 = C as Subset of T ;
assume A10: C in F ; :: thesis: B c= C
then C1 is closed_condensed by A1, Def3;
then C in { P where P is Subset of T : P is closed_condensed } ;
then A11: C in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94;
b [= c by A2, A9, A10, LATTICE3:def 16;
hence B c= C by A11, Th97; :: thesis: verum

end;

then B c= Cl (Int (meet F)) by A2, A3, A8, Th78;
hence b [= a by A4, Th97; :: thesis: verum

end;

Closed_Domains_Lattice T is complete by Th99;
hence "/\" X,(Closed_Domains_Lattice T) = Cl (Int (meet F)) by A5, A7, LATTICE3:34; :: thesis: verum

end;

thus ( X = {} implies "/\" X,(Closed_Domains_Lattice T) = [#] T ) :: thesis: verum

proof

assume A12: X = {} ; :: thesis: "/\" X,(Closed_Domains_Lattice T) = [#] T
set A = [#] T;
[#] T is closed_condensed by TDLAT_1:19;
then [#] T in { C where C is Subset of T : C is closed_condensed } ;
then A13: [#] T in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = [#] T as Element of (Closed_Domains_Lattice T) by Th94;
A14: a is_less_than X

proof

let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def 16 :: thesis: ( not b in X or a [= b )
assume b in X ; :: thesis: a [= b
hence a [= b by A12; :: thesis: verum

end;

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

proof

let b be Element of (Closed_Domains_Lattice T); :: thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Closed_Domains_of T by Th94;
assume b is_less_than X ; :: thesis: b [= a
B c= [#] T ;
hence b [= a by A13, Th97; :: thesis: verum

end;

Closed_Domains_Lattice T is complete by Th99;
hence "/\" X,(Closed_Domains_Lattice T) = [#] T by A14, A15, LATTICE3:34; :: thesis: verum

end;