:: deftheorem Def11 defines CLatt ROBBINS1:def 11 :
for L being non empty ComplLLattStr
for b₂ being strict OrthoLattStr holds
( b₂ = CLatt L iff ( the carrier of b₂ = the carrier of L & the L_join of b₂ = the L_join of L & the Compl of b₂ = the Compl of L & ( for a, b being Element of L holds the L_meet of b₂ . (a,b) = a *' b ) ) );