let L be Lattice; :: thesis: for F1, F2 being Filter of L holds F1 /\ F2 is Filter of L
let F1, F2 be Filter of L; :: thesis: F1 /\ F2 is Filter of L
consider p being Element of L such that
A1: p in F1 by FILTER_0:11;
consider q being Element of L such that
A2: q in F2 by FILTER_0:11;
( p "\/" q in F1 & p "\/" q in F2 ) by A1, A2, FILTER_0:10;
then reconsider D = F1 /\ F2 as non empty Subset of L by XBOOLE_0:def 4;
D is Filter of L

proof

let p be Element of L; :: according to FILTER_0:def 1 :: thesis: for b₁ being Element of the carrier of L holds
( ( not p in D or not b₁ in D or p "/\" b₁ in D ) & ( not p "/\" b₁ in D or ( p in D & b₁ in D ) ) )
let q be Element of L; :: thesis: ( ( not p in D or not q in D or p "/\" q in D ) & ( not p "/\" q in D or ( p in D & q in D ) ) )
( ( p in D & q in D implies ( p in F1 & q in F1 & p in F2 & q in F2 ) ) & ( p in F1 & q in F1 & p in F2 & q in F2 implies ( p in D & q in D ) ) & ( p "/\" q in F1 & p "/\" q in F2 implies ( p in F1 & q in F1 & p in F2 & q in F2 ) ) & ( p in F1 & q in F1 & p in F2 & q in F2 implies ( p "/\" q in F1 & p "/\" q in F2 ) ) & ( p "/\" q in F1 & p "/\" q in F2 implies p "/\" q in F1 /\ F2 ) & ( p "/\" q in F1 /\ F2 implies ( p "/\" q in F1 & p "/\" q in F2 ) ) ) by FILTER_0:def 1, XBOOLE_0:def 4;
hence ( ( not p in D or not q in D or p "/\" q in D ) & ( not p "/\" q in D or ( p in D & q in D ) ) ) ; :: thesis: verum

end;

hence F1 /\ F2 is Filter of L ; :: thesis: verum