let T be non empty TopSpace; :: thesis: ( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T )
thus Bottom (Domains_Lattice T) = {} T :: thesis: Top (Domains_Lattice T) = [#] T
proof
{} T is condensed by TDLAT_1:14;
then A1: {} T in { A where A is Subset of T : A is condensed } ;
then reconsider E = {} T as Element of Domains_of T by TDLAT_1:def 1;
{} T in Domains_of T by A1, TDLAT_1:def 1;
then reconsider e = {} T as Element of (Domains_Lattice T) by Th85;
for a being Element of (Domains_Lattice T) holds e "\/" a = a
proof
let a be Element of (Domains_Lattice T); :: thesis: e "\/" a = a
reconsider A = a as Element of Domains_of T by Th85;
A in Domains_of T ;
then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def 1;
then ex D being Subset of T st
( D = A & D is condensed ) ;
then A2: Int (Cl A) c= A by TOPS_1:def 6;
thus e "\/" a = (Int (Cl (E \/ A))) \/ (E \/ A) by Th86
.= a by A2, XBOOLE_1:12 ; :: thesis: verum
end;
hence Bottom (Domains_Lattice T) = {} T by LATTICE2:14; :: thesis: verum
end;
thus Top (Domains_Lattice T) = [#] T :: thesis: verum
proof
[#] T is condensed by TDLAT_1:15;
then A3: [#] T in { A where A is Subset of T : A is condensed } ;
then reconsider E = [#] T as Element of Domains_of T by TDLAT_1:def 1;
[#] T in Domains_of T by A3, TDLAT_1:def 1;
then reconsider e = [#] T as Element of (Domains_Lattice T) by Th85;
for a being Element of (Domains_Lattice T) holds e "/\" a = a
proof
let a be Element of (Domains_Lattice T); :: thesis: e "/\" a = a
reconsider A = a as Element of Domains_of T by Th85;
A in Domains_of T ;
then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def 1;
then ex D being Subset of T st
( D = A & D is condensed ) ;
then A4: A c= Cl (Int A) by TOPS_1:def 6;
thus e "/\" a = (Cl (Int (E /\ A))) /\ (E /\ A) by Th86
.= (Cl (Int A)) /\ (([#] T) /\ A) by XBOOLE_1:28
.= (Cl (Int A)) /\ A by XBOOLE_1:28
.= a by A4, XBOOLE_1:28 ; :: thesis: verum
end;
hence Top (Domains_Lattice T) = [#] T by LATTICE2:16; :: thesis: verum
end;