let L1, L2 be Lattice; :: thesis: ( ( L1 is D_Lattice & L2 is D_Lattice ) iff [:L1,L2:] is D_Lattice )
thus ( L1 is D_Lattice & L2 is D_Lattice implies [:L1,L2:] is D_Lattice ) :: thesis: ( [:L1,L2:] is D_Lattice implies ( L1 is D_Lattice & L2 is D_Lattice ) )

proof

assume ( L1 is D_Lattice & L2 is D_Lattice ) ; :: thesis: [:L1,L2:] is D_Lattice
then ( H₁(L1) is_distributive_wrt H₂(L1) & H₁(L2) is_distributive_wrt H₂(L2) ) by LATTICE2:35;
then |:H₁(L1),H₁(L2):| is_distributive_wrt |:H₂(L1),H₂(L2):| by Th30;
hence [:L1,L2:] is D_Lattice by LATTICE2:36; :: thesis: verum

end;

assume [:L1,L2:] is D_Lattice ; :: thesis: ( L1 is D_Lattice & L2 is D_Lattice )
then H₁([:L1,L2:]) is_distributive_wrt H₂([:L1,L2:]) by LATTICE2:35;
then ( H₁(L1) is_distributive_wrt H₂(L1) & H₁(L2) is_distributive_wrt H₂(L2) ) by Th30;
hence ( L1 is D_Lattice & L2 is D_Lattice ) by LATTICE2:36; :: thesis: verum