let H be non trivial H_Lattice; :: thesis: StoneS H c= bool (F_primeSet H)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in StoneS H or x in bool (F_primeSet H) )
assume x in StoneS H ; :: thesis: x in bool (F_primeSet H)
then consider p' being Element of H such that
A1: x = (StoneH H) . p' by Th15;
A2: x = { F where F is Filter of H : ( F in F_primeSet H & p' in F ) } by A1, Def6;
x c= F_primeSet H

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in F_primeSet H )
assume y in x ; :: thesis: y in F_primeSet H
then consider F being Filter of H such that
A3: ( y = F & F in F_primeSet H & p' in F ) by A2;
thus y in F_primeSet H by A3; :: thesis: verum

end;

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