rng (UFilter BL) = the carrier of (StoneBLattice BL) by Th41;
then UFilter BL is onto by FUNCT_2:def 3;
hence for b₁ being Function of BL,(StoneBLattice BL) st b₁ = UFilter BL holds
b₁ is bijective ; :: thesis: verum