:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :
for V, C being set
for b₃ being strict LattStr holds
( b₃ = SubstLatt (V,C) iff ( the carrier of b₃ = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b₃ . (A,B) = mi (A \/ B) & the L_meet of b₃ . (A,B) = mi (A ^ B) ) ) ) );