let T be TopSpace; :: thesis: Open_Domains_Lattice T is SubLattice of Domains_Lattice T
set L = Domains_Lattice T;
set OL = Open_Domains_Lattice T;
thus the carrier of (Open_Domains_Lattice T) c= the carrier of (Domains_Lattice T) by Th35; :: according to NAT_LAT:def 12 :: thesis: ( the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) & the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) )
thus the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th42; :: thesis: the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T)
thus the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th43; :: thesis: verum