let L be Lattice; :: thesis: for a being Element of L
for x being set holds
( x in (PrimeFilters L) . a iff ex F being Filter of L st
( F = x & F is prime & a in F ) )
let a be Element of L; :: thesis: for x being set holds
( x in (PrimeFilters L) . a iff ex F being Filter of L st
( F = x & F is prime & a in F ) )
let x be set ; :: thesis: ( x in (PrimeFilters L) . a iff ex F being Filter of L st
( F = x & F is prime & a in F ) )
thus ( x in (PrimeFilters L) . a implies ex F being Filter of L st
( F = x & F is prime & a in F ) ) :: thesis: ( ex F being Filter of L st
( F = x & F is prime & a in F ) implies x in (PrimeFilters L) . a )

proof

assume x in (PrimeFilters L) . a ; :: thesis: ex F being Filter of L st
( F = x & F is prime & a in F )
then x in { F1 where F1 is Filter of L : ( F1 is prime & a in F1 ) } by Def6;
then consider F being Filter of L such that
A2: F = x and
A3: F is prime and
A4: a in F ;
take F ; :: thesis: ( F = x & F is prime & a in F )
thus ( F = x & F is prime & a in F ) by A2, A3, A4; :: thesis: verum

end;

assume ex F being Filter of L st
( F = x & F is prime & a in F ) ; :: thesis: x in (PrimeFilters L) . a
then x in { F where F is Filter of L : ( F is prime & a in F ) } ;
hence x in (PrimeFilters L) . a by Def6; :: thesis: verum