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;

hence UFilter BL is Homomorphism of BL,(StoneBLattice BL) ; :: thesis: verum

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

then
( f is "\/"-preserving & f is "/\"-preserving )
by LATTICE4:def 1, LATTICE4:def 2;( 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;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

hence UFilter BL is Homomorphism of BL,(StoneBLattice BL) ; :: thesis: verum