let BL be non trivial B_Lattice; :: thesis: union (StoneR BL) = ultraset BL
consider x being Element of OpenClosedSet (StoneSpace BL);
reconsider X = x as Subset of (StoneSpace BL) ;
A1: ( X is open & X is closed ) by Th2, Th3;
then X in the topology of (StoneSpace BL) by PRE_TOPC:def 5;
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
A2: ( union B = X & B c= StoneR BL ) ;
X ` is open by A1, TOPS_1:29;
then X ` in the topology of (StoneSpace BL) by PRE_TOPC:def 5;
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
A3: ( union C = X ` & C c= StoneR BL ) ;
B \/ C c= StoneR BL by A2, A3, XBOOLE_1:8;
then union (B \/ C) c= union (StoneR BL) by ZFMISC_1:95;
then X \/ (X ` ) c= union (StoneR BL) by A2, A3, ZFMISC_1:96;
then [#] (StoneSpace BL) c= union (StoneR BL) by PRE_TOPC:18;
then A4: ultraset BL c= union (StoneR BL) by Def8;
union (StoneR BL) c= union (bool (ultraset BL)) by ZFMISC_1:95;
then union (StoneR BL) c= ultraset BL by ZFMISC_1:99;
hence union (StoneR BL) = ultraset BL by A4, XBOOLE_0:def 10; :: thesis: verum