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

A1: now :: thesis: for F, H being Filter of L holds F c= F "/\" H

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

proof

let x be object ; :: 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 Th33;
hence ( F c= F "/\" H & H c= F "/\" H ) by A1; :: thesis: verum