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

proof

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;

hence x in bool (F_primeSet H) ; :: thesis: verum