let T be TopSpace; :: thesis: Closed_Domains_Lattice T is SubLattice of Domains_Lattice T
set L = Domains_Lattice T;
set CL = Closed_Domains_Lattice T;
thus the carrier of (Closed_Domains_Lattice T) c= the carrier of (Domains_Lattice T) by Th31; :: according to NAT_LAT:def 12 :: thesis: ( the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) & the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) )
thus the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th39; :: thesis: the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T)
thus the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th40; :: thesis: verum