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: H1(L2) is_distributive_wrt H2(L2) by A2, LATTICE2:21;
H1(L1) is_distributive_wrt H2(L1) by A1, LATTICE2:21;
then |:H1(L1),H1(L2):| is_distributive_wrt |:H2(L1),H2(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: H1([:L1,L2:]) is_distributive_wrt H2([:L1,L2:]) by LATTICE2:21;
then A5: H1(L2) is_distributive_wrt H2(L2) by Th29;
H1(L1) is_distributive_wrt H2(L1) by A4, Th29;
hence ( L1 is D_Lattice & L2 is D_Lattice ) by A5, LATTICE2:22; :: thesis: verum