theorem Th33: :: OPENLATT:33

for H being non trivial H_Lattice
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)