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 SUBSET_1:4;
consider q being Element of L such that
A2: q in F2 by SUBSET_1:4;
A3: p "\/" q in F2 by A2, FILTER_0:10;
p "\/" q in F1 by A1, FILTER_0:10;
then reconsider D = F1 /\ F2 as non empty Subset of L by A3, XBOOLE_0:def 4;

now :: thesis: for p, q being Element of L holds
( ( p in F1 /\ F2 & q in F1 /\ F2 ) iff p "/\" q in F1 /\ F2 )

let p, q be Element of L; :: thesis: ( ( p in F1 /\ F2 & q in F1 /\ F2 ) iff p "/\" q in F1 /\ F2 )
( p "/\" q in F1 & p "/\" q in F2 iff ( p in F1 & q in F1 & p in F2 & q in F2 ) ) by FILTER_0:8;
hence ( ( p in F1 /\ F2 & q in F1 /\ F2 ) iff p "/\" q in F1 /\ F2 ) by XBOOLE_0:def 4; :: thesis: verum

end;

then D is Filter of L by FILTER_0:8;
hence F1 /\ F2 is Filter of L ; :: thesis: verum