let T be non empty TopSpace; :: thesis: ( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T )
thus Bottom (Open_Domains_Lattice T) = {} T :: thesis: Top (Open_Domains_Lattice T) = [#] T
proof
{} T is open_condensed by TDLAT_1:20;
then A1: {} T in { A where A is Subset of T : A is open_condensed } ;
then reconsider E = {} T as Element of Open_Domains_of T by TDLAT_1:def 9;
{} T in Open_Domains_of T by A1, TDLAT_1:def 9;
then reconsider e = {} T as Element of (Open_Domains_Lattice T) by Th102;
for a being Element of (Open_Domains_Lattice T) holds e "\/" a = a
proof
let a be Element of (Open_Domains_Lattice T); :: thesis: e "\/" a = a
reconsider A = a as Element of Open_Domains_of T by Th102;
A in Open_Domains_of T ;
then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def 9;
then A2: ex D being Subset of T st
( D = A & D is open_condensed ) ;
thus e "\/" a = Int (Cl (E \/ A)) by Th103
.= a by A2, TOPS_1:def 8 ; :: thesis: verum
end;
hence Bottom (Open_Domains_Lattice T) = {} T by LATTICE2:14; :: thesis: verum
end;
thus Top (Open_Domains_Lattice T) = [#] T :: thesis: verum
proof
[#] T is open_condensed by TDLAT_1:21;
then A3: [#] T in { A where A is Subset of T : A is open_condensed } ;
then reconsider E = [#] T as Element of Open_Domains_of T by TDLAT_1:def 9;
[#] T in Open_Domains_of T by A3, TDLAT_1:def 9;
then reconsider e = [#] T as Element of (Open_Domains_Lattice T) by Th102;
for a being Element of (Open_Domains_Lattice T) holds e "/\" a = a
proof
let a be Element of (Open_Domains_Lattice T); :: thesis: e "/\" a = a
reconsider A = a as Element of Open_Domains_of T by Th102;
thus e "/\" a = E /\ A by Th103
.= a by XBOOLE_1:28 ; :: thesis: verum
end;
hence Top (Open_Domains_Lattice T) = [#] T by LATTICE2:16; :: thesis: verum
end;