:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :
for b₁ being strict OrthoLattStr holds
( b₁ = Benzene iff ( LattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁ #) = latt B_6 & ( for x being Element of b₁
for y being Subset of 3 st x = y holds
the Compl of b₁ . x = y ` ) ) );