let L1, L2 be Lattice; :: thesis: ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )
( ( L1 is B_Lattice implies ( L1 is C_Lattice & L1 is D_Lattice ) ) & ( L1 is C_Lattice & L1 is D_Lattice implies L1 is B_Lattice ) & ( L2 is B_Lattice implies ( L2 is C_Lattice & L2 is D_Lattice ) ) & ( L2 is C_Lattice & L2 is D_Lattice implies L2 is B_Lattice ) & ( [:L1,L2:] is C_Lattice implies ( L1 is C_Lattice & L2 is C_Lattice ) ) & ( L1 is C_Lattice & L2 is C_Lattice implies [:L1,L2:] is C_Lattice ) & ( [:L1,L2:] is D_Lattice implies ( L1 is D_Lattice & L2 is D_Lattice ) ) & ( L1 is D_Lattice & L2 is D_Lattice implies [:L1,L2:] is D_Lattice ) & ( [:L1,L2:] is B_Lattice implies ( [:L1,L2:] is C_Lattice & [:L1,L2:] is D_Lattice ) ) & ( [:L1,L2:] is C_Lattice & [:L1,L2:] is D_Lattice implies [:L1,L2:] is B_Lattice ) ) by Th39, Th46;
hence ( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice ) ; :: thesis: verum