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;

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

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 )

then
D is Filter of L
by FILTER_0:8;( ( 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;( 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

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