let T be non empty TopSpace; :: thesis: ( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T )
thus Bottom (Closed_Domains_Lattice T) = {} T :: thesis: Top (Closed_Domains_Lattice T) = [#] T

proof

{} T is closed_condensed by TDLAT_1:18;
then A1: {} T in { A where A is Subset of T : A is closed_condensed } ;
then reconsider E = {} T as Element of Closed_Domains_of T by TDLAT_1:def 5;
{} T in Closed_Domains_of T by A1, TDLAT_1:def 5;
then reconsider e = {} T as Element of (Closed_Domains_Lattice T) by Th93;
for a being Element of (Closed_Domains_Lattice T) holds e "\/" a = a

proof

let a be Element of (Closed_Domains_Lattice T); :: thesis: e "\/" a = a
reconsider A = a as Element of Closed_Domains_of T by Th93;
thus e "\/" a = E \/ A by Th94
.= a ; :: thesis: verum

end;

hence Bottom (Closed_Domains_Lattice T) = {} T by LATTICE2:14; :: thesis: verum

end;

thus Top (Closed_Domains_Lattice T) = [#] T :: thesis: verum

proof

[#] T is closed_condensed by TDLAT_1:19;
then A2: [#] T in { A where A is Subset of T : A is closed_condensed } ;
then reconsider E = [#] T as Element of Closed_Domains_of T by TDLAT_1:def 5;
[#] T in Closed_Domains_of T by A2, TDLAT_1:def 5;
then reconsider e = [#] T as Element of (Closed_Domains_Lattice T) by Th93;
for a being Element of (Closed_Domains_Lattice T) holds e "/\" a = a

proof

let a be Element of (Closed_Domains_Lattice T); :: thesis: e "/\" a = a
reconsider A = a as Element of Closed_Domains_of T by Th93;
A in Closed_Domains_of T ;
then A in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def 5;
then A3: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
thus e "/\" a = Cl (Int (E /\ A)) by Th94
.= Cl (Int A) by XBOOLE_1:28
.= a by A3, TOPS_1:def 7 ; :: thesis: verum

end;

hence Top (Closed_Domains_Lattice T) = [#] T by LATTICE2:16; :: thesis: verum

end;