let H be non trivial H_Lattice; :: thesis: (StoneH H) . (Top H) = F_primeSet 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

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F_primeSet H or x in (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;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

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