let BL be non trivial B_Lattice; :: thesis: BL, StoneBLattice BL are_isomorphic
ex f being Homomorphism of BL, StoneBLattice BL st
( f = UFilter BL & f is bijective ) ;
hence BL, StoneBLattice BL are_isomorphic by LATTICE4:def 5; :: thesis: verum