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

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