:: deftheorem Def12 defines NormForm NORMFORM:def 12 :
for A being set
for b₂ being strict LattStr holds
( b₂ = NormForm A iff ( the carrier of b₂ = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b₂ . (B,C) = mi (B \/ C) & the L_meet of b₂ . (B,C) = mi (B ^ C) ) ) ) );