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

proof

set A = Cl (Int (meet F));
Cl (Int (meet F)) is closed_condensed by A1, Th75;
then Cl (Int (meet F)) in { C where C is Subset of T : C is closed_condensed } ;
then A3: 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 Th93;
A4: a is_less_than X

proof

let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def 16 :: thesis:
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b in X ; :: thesis:
then Cl (Int (meet F)) c= B by A1, A2, Th73, Th77;
hence a [= b by A3, Th96; :: thesis:

end;

assume A5: X <> {} ; :: thesis:
A6: 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:
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume A7: b is_less_than X ; :: thesis:
A8: for C being Subset of T st C in F holds
B c= C

proof

let C be Subset of T; :: thesis:
reconsider C1 = C as Subset of T ;
assume A9: C in F ; :: thesis:
then C1 is closed_condensed by A1;
then C in { P where P is Subset of T : P is closed_condensed } ;
then A10: C in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th93;
b [= c by A2, A7, A9;
hence B c= C by A10, Th96; :: thesis:

end;

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 ex C being Subset of T st
( C = B & C is closed_condensed ) ;
then B c= Cl (Int (meet F)) by A2, A5, A8, Th77;
hence b [= a by A3, Th96; :: thesis:

end;

Closed_Domains_Lattice T is complete by Th98;
hence "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) by A4, A6, LATTICE3:34; :: thesis:

end;

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

proof

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 A11: [#] T in Closed_Domains_of T by TDLAT_1:def 5;
then reconsider a = [#] T as Element of (Closed_Domains_Lattice T) by Th93;
A12: 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:
reconsider B = b as Element of Closed_Domains_of T by Th93;
assume b is_less_than X ; :: thesis:
B c= [#] T ;
hence b [= a by A11, Th96; :: thesis:

end;

assume A13: X = {} ; :: thesis:
A14: a is_less_than X by A13;
Closed_Domains_Lattice T is complete by Th98;
hence "/\" (X,(Closed_Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; :: thesis:

end;