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