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 ) )

then A4: H_{1}([:L1,L2:]) is_distributive_wrt H_{2}([:L1,L2:])
by LATTICE2:21;

then A5: H_{1}(L2) is_distributive_wrt H_{2}(L2)
by Th29;

H_{1}(L1) is_distributive_wrt H_{2}(L1)
by A4, Th29;

hence ( L1 is D_Lattice & L2 is D_Lattice ) by A5, LATTICE2:22; :: thesis: verum

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,L2:] is D_Lattice
; :: thesis: ( L1 is D_Lattice & L2 is D_Lattice )
assume that

A1: L1 is D_Lattice and

A2: L2 is D_Lattice ; :: thesis: [:L1,L2:] is D_Lattice

A3: H_{1}(L2) is_distributive_wrt H_{2}(L2)
by A2, LATTICE2:21;

H_{1}(L1) is_distributive_wrt H_{2}(L1)
by A1, LATTICE2:21;

then |:H_{1}(L1),H_{1}(L2):| is_distributive_wrt |:H_{2}(L1),H_{2}(L2):|
by A3, Th29;

hence [:L1,L2:] is D_Lattice by LATTICE2:22; :: thesis: verum

end;A1: L1 is D_Lattice and

A2: L2 is D_Lattice ; :: thesis: [:L1,L2:] is D_Lattice

A3: H

H

then |:H

hence [:L1,L2:] is D_Lattice by LATTICE2:22; :: thesis: verum

then A4: H

then A5: H

H

hence ( L1 is D_Lattice & L2 is D_Lattice ) by A5, LATTICE2:22; :: thesis: verum