let H be non trivial H_Lattice; :: thesis: (StoneH H) . (Top H) = F_primeSet H

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: F_primeSet H c= (StoneH H) . (Top H)

let x be object ; :: thesis: ( x in (StoneH H) . (Top H) implies x in F_primeSet H )
assume x in (StoneH H) . (Top H) ; :: thesis: x in F_primeSet H
then ex F being Filter of H st
( F = x & F <> the carrier of H & F is prime & Top H in F ) by Th12;
hence x in F_primeSet H ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F_primeSet H or x in (StoneH H) . (Top H) )
assume x in F_primeSet H ; :: thesis: x in (StoneH H) . (Top H)
then consider F being Filter of H such that
A1: F = x and
A2: F <> the carrier of H and
A3: F is prime ;
Top H in F by FILTER_0:11;
hence x in (StoneH H) . (Top H) by A1, A2, A3, Th12; :: thesis: verum