:: deftheorem Defx4 defines latt LATTAD_1:def 26 :
for L being non empty LattStr
for P being ClosedSubset of L
for b₃ being strict SubLattStr of L holds
( b₃ = latt (L,P) iff the carrier of b₃ = P );