let BL be non trivial B_Lattice; :: thesis: for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
let p be Subset of (StoneSpace BL); :: thesis: ( p in StoneR BL implies p is open )
assume A1: p in StoneR BL ; :: thesis: p is open
then A2: {p} is Subset-Family of (ultraset BL) by SUBSET_1:41;
A3: {p} c= StoneR BL by A1, ZFMISC_1:31;
union {p} = p by ZFMISC_1:25;
then p in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } by A2, A3;
then p in the topology of (StoneSpace BL) by Def8;
hence p is open by PRE_TOPC:def 2; :: thesis: verum