let BL be non trivial B_Lattice; :: thesis: StoneR BL c= OpenClosedSet (StoneSpace BL)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in StoneR BL or x in OpenClosedSet (StoneSpace BL) )
assume A1: x in StoneR BL ; :: thesis: x in OpenClosedSet (StoneSpace BL)
then reconsider p = x as Subset of (StoneSpace BL) by Def8;
A2: p is open by A1, Lm1;
p is closed

proof

set ST = StoneSpace BL;
A3: [#] (StoneSpace BL) = ultraset BL by Def8;
consider a being Element of BL such that
A4: (UFilter BL) . a = p by A1, Th23;
p ` = (UFilter BL) . (a `) by A3, A4, Th25;
then p ` in StoneR BL by Th23;
then p ` is open by Lm1;
hence p is closed by TOPS_1:3; :: thesis: verum

end;

hence x in OpenClosedSet (StoneSpace BL) by A2; :: thesis: verum