let L1, L2 be Lattice; :: thesis: ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )
A1: ( [:L1,L2:] is D_Lattice iff ( L1 is D_Lattice & L2 is D_Lattice ) ) by Th38;
( [:L1,L2:] is C_Lattice iff ( L1 is C_Lattice & L2 is C_Lattice ) ) by Th45;
hence ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice ) by A1; :: thesis: verum