let L be Lattice; :: thesis: for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
let F, H be Filter of L; :: thesis: ( F c= F "/\" H & H c= F "/\" H )

A1: now

let F, H be Filter of L; :: thesis: F c= F "/\" H
thus F c= F "/\" H :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in F "/\" H )
assume A2: x in F ; :: thesis: x in F "/\" H
then reconsider i = x as Element of L ;
consider p being Element of L such that
A3: p in H by SUBSET_1:4;
i [= i "\/" p by LATTICES:5;
then A4: i "/\" (i "\/" p) = i by LATTICES:4;
p [= p "\/" i by LATTICES:5;
then i "\/" p in H by A3, Th9;
hence x in F "/\" H by A2, A4; :: thesis: verum

end;

end;

F "/\" H = H "/\" F by Th46;
hence ( F c= F "/\" H & H c= F "/\" H ) by A1; :: thesis: verum