reconsider g = UFilter BL as Function of the carrier of BL,(bool (ultraset BL)) ;
set SL = StoneBLattice BL;
rng g = StoneR BL ;
then rng g c= OpenClosedSet (StoneSpace BL) by Lm2;
then reconsider f = UFilter BL as Function of the carrier of BL, the carrier of (StoneBLattice BL) by FUNCT_2:6;
now :: thesis: for p, q being Element of BL holds
( f . (p "\/" q) = (f . p) "\/" (f . q) & f . (p "/\" q) = (f . p) "/\" (f . q) )
let p, q be Element of BL; :: thesis: ( f . (p "\/" q) = (f . p) "\/" (f . q) & f . (p "/\" q) = (f . p) "/\" (f . q) )
thus f . (p "\/" q) = (f . p) \/ (f . q) by Th21
.= (f . p) "\/" (f . q) by Def2 ; :: thesis: f . (p "/\" q) = (f . p) "/\" (f . q)
thus f . (p "/\" q) = (f . p) /\ (f . q) by Th20
.= (f . p) "/\" (f . q) by Def3 ; :: thesis: verum
end;
then ( f is "\/"-preserving & f is "/\"-preserving ) by LATTICE4:def 1, LATTICE4:def 2;
hence UFilter BL is Homomorphism of BL,(StoneBLattice BL) ; :: thesis: verum