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

proof

assume that
A1: L1 is C_Lattice and
A2: L2 is C_Lattice ; :: thesis: [:L1,L2:] is C_Lattice
reconsider L = [:L1,L2:] as 01_Lattice by A1, A2, Th42;
L is complemented

proof

let a be Element of ; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of L st b₁ is_a_complement_of a
consider p1 being Element of , p2 being Element of such that
A3: a = [p1,p2] by DOMAIN_1:9;
consider q1 being Element of such that
A4: q1 is_a_complement_of p1 by A1, LATTICES:def 19;
consider q2 being Element of such that
A5: q2 is_a_complement_of p2 by A2, LATTICES:def 19;
reconsider b = [q1,q2] as Element of ;
take b ; :: thesis: b is_a_complement_of a
thus b is_a_complement_of a by A1, A2, A3, A4, A5, Th45; :: thesis: verum

end;

hence [:L1,L2:] is C_Lattice ; :: thesis: verum

end;

assume A6: [:L1,L2:] is C_Lattice ; :: thesis: ( L1 is C_Lattice & L2 is C_Lattice )
then reconsider C1 = L1, C2 = L2 as 01_Lattice by Th42;
C1 is complemented

proof

consider p2' being Element of ;
let p1' be Element of ; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of C1 st b₁ is_a_complement_of p1'
reconsider p1 = p1' as Element of ;
reconsider p2 = p2' as Element of ;
consider b being Element of such that
A7: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;
consider q1 being Element of , q2 being Element of such that
A8: b = [q1,q2] by DOMAIN_1:9;
reconsider q1' = q1 as Element of ;
take q1' ; :: thesis: q1' is_a_complement_of p1'
thus q1' is_a_complement_of p1' by A7, A8, Th45; :: thesis: verum

end;

hence L1 is C_Lattice ; :: thesis: L2 is C_Lattice
C2 is complemented

proof

consider p1' being Element of ;
let p2' be Element of ; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of C2 st b₁ is_a_complement_of p2'
reconsider p1 = p1' as Element of ;
reconsider p2 = p2' as Element of ;
consider b being Element of such that
A9: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;
consider q1 being Element of , q2 being Element of such that
A10: b = [q1,q2] by DOMAIN_1:9;
reconsider q2' = q2 as Element of ;
take q2' ; :: thesis: q2' is_a_complement_of p2'
thus q2' is_a_complement_of p2' by A9, A10, Th45; :: thesis: verum

end;

hence L2 is C_Lattice ; :: thesis: verum