let BL be non trivial B_Lattice; :: thesis: UFilter BL is bijective
UFilter BL is one-to-one by Th29;
then A1: UFilter BL is one-to-one ;
rng (UFilter BL) = the carrier of (StoneBLattice BL) by Th41;
then UFilter BL is onto by FUNCT_2:def 3;
hence UFilter BL is bijective by A1; :: thesis: verum