let L be D_Lattice; :: thesis: for a being Element of L

for x being set holds

( x in SF_have a iff ( x is Filter of L & a in x ) )

let a be Element of L; :: thesis: for x being set holds

( x in SF_have a iff ( x is Filter of L & a in x ) )

let x be set ; :: thesis: ( x in SF_have a iff ( x is Filter of L & a in x ) )

( x in SF_have a iff ex F being Filter of L st

( F = x & a in F ) ) ;

hence ( x in SF_have a iff ( x is Filter of L & a in x ) ) ; :: thesis: verum

for x being set holds

( x in SF_have a iff ( x is Filter of L & a in x ) )

let a be Element of L; :: thesis: for x being set holds

( x in SF_have a iff ( x is Filter of L & a in x ) )

let x be set ; :: thesis: ( x in SF_have a iff ( x is Filter of L & a in x ) )

( x in SF_have a iff ex F being Filter of L st

( F = x & a in F ) ) ;

hence ( x in SF_have a iff ( x is Filter of L & a in x ) ) ; :: thesis: verum