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 Th32;

then reconsider f = g as Function of the carrier of H, the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:6;

hence StoneH H is Homomorphism of H,(Open_setLatt (HTopSpace H)) ; :: thesis: verum

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 Th32;

then reconsider f = g as Function of the carrier of H, the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:6;

now :: thesis: for p9, q9 being Element of H holds

( f . (p9 "\/" q9) = (f . p9) "\/" (f . q9) & f . (p9 "/\" q9) = (f . p9) "/\" (f . q9) )

then
( f is "\/"-preserving & f is "/\"-preserving )
;( f . (p9 "\/" q9) = (f . p9) "\/" (f . q9) & f . (p9 "/\" q9) = (f . p9) "/\" (f . q9) )

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 Th14

.= (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 Th15

.= (f . p9) "/\" (f . q9) by Def3 ; :: thesis: verum

end;thus f . (p9 "\/" q9) = ((StoneH H) . p9) \/ ((StoneH H) . q9) by Th14

.= (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 Th15

.= (f . p9) "/\" (f . q9) by Def3 ; :: thesis: verum

hence StoneH H is Homomorphism of H,(Open_setLatt (HTopSpace H)) ; :: thesis: verum