:: deftheorem defines Kleene PARTPR_1:def 18 :
for L being non empty OrthoLattStr holds
( L is Kleene iff for x, y being Element of L holds x "/\" (x `) [= y "\/" (y `) );