let B be B_Lattice; :: thesis: for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
let FB, HB be Filter of B; :: thesis: <.(FB \/ HB).) = FB "/\" HB
FB "/\" HB = <.(FB "/\" HB).) by Th21;
hence <.(FB \/ HB).) = FB "/\" HB by Th37; :: thesis: verum