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: now :: thesis: for r being Element of (Open_setLatt (HTopSpace H)) st ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 holds
r [= (StoneH H) . (p9 => q9)

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
A3: 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 Th6;
then ((StoneH H) . p9) /\ (union A) c= (StoneH H) . q9 by A3, Def3;
then A4: union (INTERSECTION ({((StoneH H) . p9)},A)) c= (StoneH H) . q9 by SETFAM_1:25;

now :: thesis: for x being set st x in A holds
x c= (StoneH H) . (p9 => q9)

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

end;

then union A c= (StoneH H) . (p9 => q9) by ZFMISC_1:76;
hence r [= (StoneH H) . (p9 => q9) by A3, Th6; :: thesis: verum

end;

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