let L be D_Lattice; :: thesis: for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let F be Filter of L; :: thesis: for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let a be Element of L; :: thesis: ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
(StoneH L) . a = { F0 where F0 is Filter of L : ( F0 in F_primeSet L & a in F0 ) } by Def6;
then ( F in (StoneH L) . a iff ex F0 being Filter of L st
( F = F0 & F0 in F_primeSet L & a in F0 ) ) ;
hence ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) ) ; :: thesis: verum