:: deftheorem defSublattice defines Z_Sublattice ZMODLAT1:def 9 :
for L, b₂ being Z_Lattice holds
( b₂ is Z_Sublattice of L iff ( the carrier of b₂ c= the carrier of L & 0. b₂ = 0. L & the addF of b₂ = the addF of L || the carrier of b₂ & the lmult of b₂ = the lmult of L | [: the carrier of INT.Ring, the carrier of b₂:] & the scalar of b₂ = the scalar of L || the carrier of b₂ ) );