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 3; :: thesis: verum