let L be Lattice; 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; ( 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; ( ( 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 A1:
( ( 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 ) )
; D is Filter of L
then
for p, q being Element of L st p [= q & p in D holds
q in D
;
hence
D is Filter of L
by A1, LATTICES:def 23, LATTICES:def 24; verum