:: deftheorem Def12 defines SubLattice NAT_LAT:def 12 :
for L, b₂ being Lattice holds
( b₂ is SubLattice of L iff ( the carrier of b₂ c= the carrier of L & the L_join of b₂ = the L_join of L || the carrier of b₂ & the L_meet of b₂ = the L_meet of L || the carrier of b₂ ) );