theorem Th12: :: LATSTONE:19

for L being distributive bounded pseudocomplemented Lattice holds
( L is satisfying_Stone_identity iff for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) )