let L be Lattice; :: thesis: for D being non empty Subset of L holds
( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) ) )
let D be non empty Subset of L; :: thesis: ( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) ) )
thus ( D is Filter of L implies ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) ) ) :: thesis: ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) implies D is Filter of L )

proof

assume A1: D is Filter of L ; :: thesis: ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) )
hence for p, q being Element of L st p in D & q in D holds
p "/\" q in D by Def1; :: thesis: for p, q being Element of L st p in D & p [= q holds
q in D
let p, q be Element of L; :: thesis: ( p in D & p [= q implies q in D )
assume A2: ( p in D & p [= q ) ; :: thesis: q in D
then p "/\" q = p by LATTICES:21;
hence q in D by A1, A2, Def1; :: thesis: verum

end;

assume that
A3: for p, q being Element of L st p in D & q in D holds
p "/\" q in D and
A4: for p, q being Element of L st p in D & p [= q holds
q in D ; :: thesis: D is Filter of L
let p be Element of L; :: according to FILTER_0:def 1 :: thesis: for q being Element of L holds
( ( p in D & q in D ) iff p "/\" q in D )
let q be Element of L; :: thesis: ( ( p in D & q in D ) iff p "/\" q in D )
( p "/\" q [= p & q "/\" p [= q & q "/\" p = p "/\" q ) by LATTICES:23;
hence ( ( p in D & q in D ) iff p "/\" q in D ) by A3, A4; :: thesis: verum