theorem :: LATSTONE:20

for L being distributive bounded pseudocomplemented Lattice holds
( L is satisfying_Stone_identity iff for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "\/" b in Skeleton L )