let L be Lattice; :: thesis: ( L is B_Lattice iff L .: is B_Lattice )
A1: ( L is distributive iff L .: is distributive ) by LATTICE2:50;
( L is C_Lattice iff L .: is C_Lattice ) by Th52;
hence ( L is B_Lattice iff L .: is B_Lattice ) by A1; :: thesis: verum