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 ) ) ) by LATTICES:def 23, LATTICES:def 24; :: 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 )
assume A4: ( ( 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: D is Filter of L
then for p, q being Element of L st p [= q & p in D holds
q in D ;
then ( D is final & D is meet-closed ) by LATTICES:def 23, LATTICES:def 24, A4;
hence D is Filter of L ; :: thesis: verum