:: deftheorem Defx1 defines SubLattStr LATTAD_1:def 23 :
for L being non empty LattStr
for b₂ being LattStr holds
( b₂ is SubLattStr 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₂ ) );