:: deftheorem SatStone defines satisfying_Stone_identity LATSTONE:def 5 :
for L being non empty LattStr holds
( L is satisfying_Stone_identity iff for x being Element of L holds (x *) "\/" ((x *) *) = Top L );