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:8;

now

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 Th24
.= (f . p) "\/" (f . q) by Def2 ; :: thesis: f . (p "/\" q) = (f . p) "/\" (f . q)
thus f . (p "/\" q) = (f . p) /\ (f . q) by Th23
.= (f . p) "/\" (f . q) by Def3 ; :: thesis: verum

end;

hence UFilter BL is Homomorphism of BL, StoneBLattice BL by LATTICE4:def 1; :: thesis: verum