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

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