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

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

hence
x in OpenClosedSet (StoneSpace BL)
by A2; :: thesis: verum
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;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