let H be non trivial H_Lattice; :: thesis: for p9, q9 being Element of H holds () . (p9 => q9) = (() . p9) => (() . q9)
let p9, q9 be Element of H; :: thesis: () . (p9 => q9) = (() . p9) => (() . q9)
A1: the carrier of () = { () where A is Subset of () : verum } by Def12;
A2: now :: thesis: for r being Element of () st (() . p9) "/\" r [= () . q9 holds
r [= () . (p9 => q9)
let r be Element of (); :: thesis: ( (() . p9) "/\" r [= () . q9 implies r [= () . (p9 => q9) )
r in the carrier of () ;
then consider A being Subset of () such that
A3: r = union A by A1;
assume ((StoneH H) . p9) "/\" r [= () . q9 ; :: thesis: r [= () . (p9 => q9)
then ((StoneH H) . p9) "/\" r c= () . q9 by Th6;
then ((StoneH H) . p9) /\ () c= () . q9 by ;
then A4: union (INTERSECTION ({(() . p9)},A)) c= () . q9 by SETFAM_1:25;
now :: thesis: for x being set st x in A holds
x c= () . (p9 => q9)
let x be set ; :: thesis: ( x in A implies x c= () . (p9 => q9) )
assume A5: x in A ; :: thesis: x c= () . (p9 => q9)
then consider x9 being Element of H such that
A6: x = () . x9 by Th13;
(StoneH H) . p9 in {(() . p9)} by TARSKI:def 1;
then ((StoneH H) . p9) /\ x in INTERSECTION ({(() . p9)},A) by ;
then ((StoneH H) . p9) /\ (() . x9) c= () . q9 by ;
then (StoneH H) . (p9 "/\" x9) c= () . q9 by Th15;
then (StoneH H) . (p9 "/\" x9) [= () . q9 by Th6;
then p9 "/\" x9 [= q9 by LATTICE4:5;
then x9 [= p9 => q9 by FILTER_0:def 7;
then (StoneH H) . x9 [= () . (p9 => q9) by LATTICE4:4;
hence x c= () . (p9 => q9) by ; :: thesis: verum
end;
then union A c= () . (p9 => q9) by ZFMISC_1:76;
hence r [= () . (p9 => q9) by ; :: thesis: verum
end;
p9 "/\" (p9 => q9) [= q9 by FILTER_0:def 7;
then (StoneH H) . (p9 "/\" (p9 => q9)) [= () . q9 by LATTICE4:4;
then ((StoneH H) . p9) "/\" (() . (p9 => q9)) [= () . q9 by LATTICE4:def 2;
hence (StoneH H) . (p9 => q9) = (() . p9) => (() . q9) by ; :: thesis: verum