theorem Th53: :: FILTER_2:53

for L being Lattice holds
( L is B_Lattice iff L .: is B_Lattice )