let H be non trivial H_Lattice; :: thesis: for p', q' being Element of H holds (StoneH H) . (p' => q') = ((StoneH H) . p') => ((StoneH H) . q')
let p', q' be Element of H; :: thesis: (StoneH H) . (p' => q') = ((StoneH H) . p') => ((StoneH H) . q')
A1: StoneH H is one-to-one by Th25;
A2: the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
p' "/\" (p' => q') [= q' by FILTER_0:def 8;
then (StoneH H) . (p' "/\" (p' => q')) [= (StoneH H) . q' by LATTICE4:7;
then A3: ((StoneH H) . p') "/\" ((StoneH H) . (p' => q')) [= (StoneH H) . q' by LATTICE4:def 1;

now

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

now

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

end;

then union A c= (StoneH H) . (p' => q') by ZFMISC_1:94;
hence r [= (StoneH H) . (p' => q') by A5, Th7; :: thesis: verum

end;

hence (StoneH H) . (p' => q') = ((StoneH H) . p') => ((StoneH H) . q') by A3, FILTER_0:def 8; :: thesis: verum