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