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: F "/\" H = H "/\" F by Th46;

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 Th11;
( i [= i "\/" p & p [= p "\/" i & p "\/" i = i "\/" p ) by LATTICES:22;
then ( i "\/" p in H & i "/\" (i "\/" p) = i & i "/\" (i "\/" p) = (i "\/" p) "/\" i ) by A3, Th9, LATTICES:21;
hence x in F "/\" H by A2; :: thesis: verum

end;

end;

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