let BL be non trivial B_Lattice; :: thesis: ex T being non empty TopSpace st BL, OpenClosedSetLatt T are_isomorphic
reconsider T = StoneSpace BL as non empty TopSpace ;
take T ; :: thesis: BL, OpenClosedSetLatt T are_isomorphic
OpenClosedSetLatt T = StoneBLattice BL ;
hence BL, OpenClosedSetLatt T are_isomorphic by Th35; :: thesis: verum