:: deftheorem Def9 defines Field LATTICE4:def 10 :
for BL being Boolean Lattice
for b₂ being non empty Subset of BL holds
( b₂ is Field of BL iff for a, b being Element of BL st a in b₂ & b in b₂ holds
( a "/\" b in b₂ & a ` in b₂ ) );