let BL be non trivial B_Lattice; :: thesis: union (StoneR BL) = ultraset BL
set x = the Element of OpenClosedSet (StoneSpace BL);
reconsider X = the Element of OpenClosedSet (StoneSpace BL) as Subset of (StoneSpace BL) ;
A1: X is open by Th1;
A2: X is closed by Th2;
X in the topology of (StoneSpace BL) by A1, PRE_TOPC:def 2;
then X in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } by Def8;
then consider B being Subset-Family of (ultraset BL) such that
A3: union B = X and
A4: B c= StoneR BL ;
X ` is open by A2;
then X ` in the topology of (StoneSpace BL) by PRE_TOPC:def 2;
then X ` in { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } by Def8;
then consider C being Subset-Family of (ultraset BL) such that
A5: union C = X ` and
A6: C c= StoneR BL ;
B \/ C c= StoneR BL by A4, A6, XBOOLE_1:8;
then union (B \/ C) c= union (StoneR BL) by ZFMISC_1:77;
then X \/ (X `) c= union (StoneR BL) by A3, A5, ZFMISC_1:78;
then [#] (StoneSpace BL) c= union (StoneR BL) by PRE_TOPC:2;
then A7: ultraset BL c= union (StoneR BL) by Def8;
union (StoneR BL) c= union (bool (ultraset BL)) by ZFMISC_1:77;
then union (StoneR BL) c= ultraset BL by ZFMISC_1:81;
hence union (StoneR BL) = ultraset BL by A7; :: thesis: verum