let H be non trivial H_Lattice; :: thesis: for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
let p9, q9 be Element of H; :: thesis: (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
A1: the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
A2: StoneH H is one-to-one ;

A3: now

let r be Element of (Open_setLatt (HTopSpace H)); :: thesis: ( ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 implies r [= (StoneH H) . (p9 => q9) )
r in the carrier of (Open_setLatt (HTopSpace H)) ;
then consider A being Subset of (StoneS H) such that
A4: r = union A by A1;
assume ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 ; :: thesis: r [= (StoneH H) . (p9 => q9)
then ((StoneH H) . p9) "/\" r c= (StoneH H) . q9 by Th7;
then ((StoneH H) . p9) /\ (union A) c= (StoneH H) . q9 by A4, Def3;
then A5: union (INTERSECTION {((StoneH H) . p9)},A) c= (StoneH H) . q9 by SETFAM_1:36;

now

let x be set ; :: thesis: ( x in A implies x c= (StoneH H) . (p9 => q9) )
assume A6: x in A ; :: thesis: x c= (StoneH H) . (p9 => q9)
then consider x9 being Element of H such that
A7: x = (StoneH H) . x9 by Th15;
(StoneH H) . p9 in {((StoneH H) . p9)} by TARSKI:def 1;
then ((StoneH H) . p9) /\ x in INTERSECTION {((StoneH H) . p9)},A by A6, SETFAM_1:def 5;
then ((StoneH H) . p9) /\ ((StoneH H) . x9) c= (StoneH H) . q9 by A5, A7, SETFAM_1:56;
then (StoneH H) . (p9 "/\" x9) c= (StoneH H) . q9 by Th17;
then (StoneH H) . (p9 "/\" x9) [= (StoneH H) . q9 by Th7;
then p9 "/\" x9 [= q9 by A2, LATTICE4:8;
then x9 [= p9 => q9 by FILTER_0:def 8;
then (StoneH H) . x9 [= (StoneH H) . (p9 => q9) by LATTICE4:7;
hence x c= (StoneH H) . (p9 => q9) by A7, Th7; :: thesis: verum

end;

then union A c= (StoneH H) . (p9 => q9) by ZFMISC_1:94;
hence r [= (StoneH H) . (p9 => q9) by A4, Th7; :: thesis: verum

end;

p9 "/\" (p9 => q9) [= q9 by FILTER_0:def 8;
then (StoneH H) . (p9 "/\" (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:7;
then ((StoneH H) . p9) "/\" ((StoneH H) . (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:def 1;
hence (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by A3, FILTER_0:def 8; :: thesis: verum