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;

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

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)

p9 "/\" (p9 => q9) [= q9
by FILTER_0:def 7;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;

hence r [= (StoneH H) . (p9 => q9) by A3, Th6; :: thesis: verum

end;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)

then
union A c= (StoneH H) . (p9 => q9)
by ZFMISC_1:76;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;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

hence r [= (StoneH H) . (p9 => q9) by A3, Th6; :: thesis: verum

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