let H be non trivial H_Lattice; :: thesis: StoneS H c= bool (F_primeSet H)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in StoneS H or x in bool (F_primeSet H) )

reconsider xx = x as set by TARSKI:1;

assume x in StoneS H ; :: thesis: x in bool (F_primeSet H)

then consider p9 being Element of H such that

A1: x = (StoneH H) . p9 by Th13;

A2: x = { F where F is Filter of H : ( F in F_primeSet H & p9 in F ) } by A1, Def6;

xx c= F_primeSet H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in StoneS H or x in bool (F_primeSet H) )

reconsider xx = x as set by TARSKI:1;

assume x in StoneS H ; :: thesis: x in bool (F_primeSet H)

then consider p9 being Element of H such that

A1: x = (StoneH H) . p9 by Th13;

A2: x = { F where F is Filter of H : ( F in F_primeSet H & p9 in F ) } by A1, Def6;

xx c= F_primeSet H

proof

hence
x in bool (F_primeSet H)
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in F_primeSet H )

assume y in xx ; :: thesis: y in F_primeSet H

then ex F being Filter of H st

( y = F & F in F_primeSet H & p9 in F ) by A2;

hence y in F_primeSet H ; :: thesis: verum

end;assume y in xx ; :: thesis: y in F_primeSet H

then ex F being Filter of H st

( y = F & F in F_primeSet H & p9 in F ) by A2;

hence y in F_primeSet H ; :: thesis: verum