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

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