let H be non trivial H_Lattice; :: thesis: StoneH H preserves_implication
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by Th39;
hence StoneH H preserves_implication by LATTICE4:def 6; :: thesis: verum