let L be Lattice; :: thesis: ( L is B_Lattice iff L .: is B_Lattice )
( ( L is C_Lattice implies L .: is C_Lattice ) & ( L .: is C_Lattice implies L is C_Lattice ) & ( L is distributive implies L .: is distributive ) & ( L .: is distributive implies L is distributive ) & ( L is C_Lattice & L is distributive implies L is B_Lattice ) & ( L is B_Lattice implies ( L is C_Lattice & L is distributive ) ) & ( L .: is C_Lattice & L .: is distributive implies L .: is B_Lattice ) & ( L .: is B_Lattice implies ( L .: is C_Lattice & L .: is distributive ) ) ) by Th53, LATTICE2:65;
hence ( L is B_Lattice iff L .: is B_Lattice ) ; :: thesis: verum