let I be I_Lattice; :: thesis: for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
let F1, F2 be Filter of I; :: thesis: <.(F1 \/ F2).) = F1 "/\" F2
F1 "/\" F2 = <.(F1 "/\" F2).) by Th21;
hence <.(F1 \/ F2).) = F1 "/\" F2 by Th37; :: thesis: verum