theorem :: OPENLATT:26

for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )