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 that
A1: L1 is D_Lattice and
A2: L2 is D_Lattice ; :: thesis: [:L1,L2:] is D_Lattice
A3: H₁(L2) is_distributive_wrt H₂(L2) by A2, LATTICE2:21;
H₁(L1) is_distributive_wrt H₂(L1) by A1, LATTICE2:21;
then |:H₁(L1),H₁(L2):| is_distributive_wrt |:H₂(L1),H₂(L2):| by A3, Th29;
hence [:L1,L2:] is D_Lattice by LATTICE2:22; :: thesis: verum

end;

assume [:L1,L2:] is D_Lattice ; :: thesis: ( L1 is D_Lattice & L2 is D_Lattice )
then A4: H₁([:L1,L2:]) is_distributive_wrt H₂([:L1,L2:]) by LATTICE2:21;
then A5: H₁(L2) is_distributive_wrt H₂(L2) by Th29;
H₁(L1) is_distributive_wrt H₂(L1) by A4, Th29;
hence ( L1 is D_Lattice & L2 is D_Lattice ) by A5, LATTICE2:22; :: thesis: verum