let L be D_Lattice; :: thesis: for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let a be Element of L; :: thesis: for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let x be set ; :: thesis: ( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
A1: (StoneH L) . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } by Def6;

hereby :: thesis: ( ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) implies x in (StoneH L) . a )

assume x in (StoneH L) . a ; :: thesis: ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F )
then consider F being Filter of L such that
A2: x = F and
A3: F in F_primeSet L and
A4: a in F by A1;
A5: F is prime by A3, Th10;
F <> the carrier of L by A3, Th10;
hence ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) by A2, A4, A5; :: thesis: verum

end;

given F being Filter of L such that A6: F = x and
A7: F <> the carrier of L and
A8: F is prime and
A9: a in F ; :: thesis: x in (StoneH L) . a
F in F_primeSet L by A7, A8;
hence x in (StoneH L) . a by A1, A6, A9; :: thesis: verum