let L be Lattice; :: thesis: L is SubLattice of L
thus the carrier of L c= the carrier of L ; :: according to NAT_LAT:def 16 :: thesis: ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )
thus ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L ) by Lm8; :: thesis: verum