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

proof

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

proof

let b be Element of (Domains_Lattice T); :: according to LATTICE3:def 16 :: thesis: ( not b in X or a [= b )
reconsider B = b as Element of Domains_of T by Th85;
assume b in X ; :: thesis: a [= b
then (meet F) /\ (Cl (Int (meet F))) c= B by A2, Th70;
hence a [= b by A3, Th88; :: thesis: verum

end;

assume A5: X <> {} ; :: thesis: "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F)))
A6: for b being Element of (Domains_Lattice T) st b is_less_than X holds
b [= a

proof

let b be Element of (Domains_Lattice T); :: thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Domains_of T by Th85;
assume A7: b is_less_than X ; :: thesis: b [= a
A8: 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 A9: C in F ; :: thesis: B c= C
then C1 is condensed by A1;
then C in { P where P is Subset of T : P is condensed } ;
then A10: C in Domains_of T by TDLAT_1:def 1;
then reconsider c = C as Element of (Domains_Lattice T) by Th85;
b [= c by A2, A7, A9;
hence B c= C by A10, Th88; :: thesis: verum

end;

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

end;

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

end;

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

proof

set A = [#] T;
[#] T is condensed by TDLAT_1:15;
then [#] T in { C where C is Subset of T : C is condensed } ;
then A11: [#] T in Domains_of T by TDLAT_1:def 1;
then reconsider a = [#] T as Element of (Domains_Lattice T) by Th85;
A12: for b being Element of (Domains_Lattice T) st b is_less_than X holds
b [= a

proof

let b be Element of (Domains_Lattice T); :: thesis: ( b is_less_than X implies b [= a )
reconsider B = b as Element of Domains_of T by Th85;
assume b is_less_than X ; :: thesis: b [= a
B c= [#] T ;
hence b [= a by A11, Th88; :: thesis: verum

end;

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

end;