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 12 :: 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 Lm5; :: thesis: verum