set LH = Open_setLatt (HTopSpace H);
reconsider g = StoneH H as Function of the carrier of H, the carrier of (StoneLatt H) ;
StoneS H c= the carrier of (Open_setLatt (HTopSpace H)) by Th37;
then reconsider f = g as Function of the carrier of H, the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:6;

now

let p9, q9 be Element of H; :: thesis: ( f . (p9 "\/" q9) = (f . p9) "\/" (f . q9) & f . (p9 "/\" q9) = (f . p9) "/\" (f . q9) )
thus f . (p9 "\/" q9) = ((StoneH H) . p9) \/ ((StoneH H) . q9) by Th16
.= (f . p9) "\/" (f . q9) by Def2 ; :: thesis: f . (p9 "/\" q9) = (f . p9) "/\" (f . q9)
thus f . (p9 "/\" q9) = ((StoneH H) . p9) /\ ((StoneH H) . q9) by Th17
.= (f . p9) "/\" (f . q9) by Def3 ; :: thesis: verum

end;

hence StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H) by LATTICE4:def 1; :: thesis: verum