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

then reconsider C1 = L1, C2 = L2 as 01_Lattice by Th41;

C1 is complemented

C2 is complemented

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 A6:
[:L1,L2:] is C_Lattice
; :: thesis: ( L1 is C_Lattice & L2 is C_Lattice )
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, Th41;

L is complemented

end;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, Th41;

L is complemented

proof

hence
[:L1,L2:] is C_Lattice
; :: thesis: verum
let a be Element of L; :: according to LATTICES:def 19 :: thesis: ex b_{1} being Element of the carrier of L st b_{1} is_a_complement_of a

consider p1 being Element of L1, p2 being Element of L2 such that

A3: a = [p1,p2] by DOMAIN_1:1;

consider q1 being Element of L1 such that

A4: q1 is_a_complement_of p1 by A1, LATTICES:def 19;

consider q2 being Element of L2 such that

A5: q2 is_a_complement_of p2 by A2, LATTICES:def 19;

reconsider b = [q1,q2] as Element of L ;

take b ; :: thesis: b is_a_complement_of a

thus b is_a_complement_of a by A1, A2, A3, A4, A5, Th44; :: thesis: verum

end;consider p1 being Element of L1, p2 being Element of L2 such that

A3: a = [p1,p2] by DOMAIN_1:1;

consider q1 being Element of L1 such that

A4: q1 is_a_complement_of p1 by A1, LATTICES:def 19;

consider q2 being Element of L2 such that

A5: q2 is_a_complement_of p2 by A2, LATTICES:def 19;

reconsider b = [q1,q2] as Element of L ;

take b ; :: thesis: b is_a_complement_of a

thus b is_a_complement_of a by A1, A2, A3, A4, A5, Th44; :: thesis: verum

then reconsider C1 = L1, C2 = L2 as 01_Lattice by Th41;

C1 is complemented

proof

hence
L1 is C_Lattice
; :: thesis: L2 is C_Lattice
set p29 = the Element of C2;

let p19 be Element of C1; :: according to LATTICES:def 19 :: thesis: ex b_{1} being Element of the carrier of C1 st b_{1} is_a_complement_of p19

reconsider p1 = p19 as Element of L1 ;

reconsider p2 = the Element of C2 as Element of L2 ;

consider b being Element of [:L1,L2:] such that

A7: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;

consider q1 being Element of L1, q2 being Element of L2 such that

A8: b = [q1,q2] by DOMAIN_1:1;

reconsider q19 = q1 as Element of C1 ;

take q19 ; :: thesis: q19 is_a_complement_of p19

thus q19 is_a_complement_of p19 by A7, A8, Th44; :: thesis: verum

end;let p19 be Element of C1; :: according to LATTICES:def 19 :: thesis: ex b

reconsider p1 = p19 as Element of L1 ;

reconsider p2 = the Element of C2 as Element of L2 ;

consider b being Element of [:L1,L2:] such that

A7: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;

consider q1 being Element of L1, q2 being Element of L2 such that

A8: b = [q1,q2] by DOMAIN_1:1;

reconsider q19 = q1 as Element of C1 ;

take q19 ; :: thesis: q19 is_a_complement_of p19

thus q19 is_a_complement_of p19 by A7, A8, Th44; :: thesis: verum

C2 is complemented

proof

hence
L2 is C_Lattice
; :: thesis: verum
set p19 = the Element of C1;

let p29 be Element of C2; :: according to LATTICES:def 19 :: thesis: ex b_{1} being Element of the carrier of C2 st b_{1} is_a_complement_of p29

reconsider p1 = the Element of C1 as Element of L1 ;

reconsider p2 = p29 as Element of L2 ;

consider b being Element of [:L1,L2:] such that

A9: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;

consider q1 being Element of L1, q2 being Element of L2 such that

A10: b = [q1,q2] by DOMAIN_1:1;

reconsider q29 = q2 as Element of C2 ;

take q29 ; :: thesis: q29 is_a_complement_of p29

thus q29 is_a_complement_of p29 by A9, A10, Th44; :: thesis: verum

end;let p29 be Element of C2; :: according to LATTICES:def 19 :: thesis: ex b

reconsider p1 = the Element of C1 as Element of L1 ;

reconsider p2 = p29 as Element of L2 ;

consider b being Element of [:L1,L2:] such that

A9: b is_a_complement_of [p1,p2] by A6, LATTICES:def 19;

consider q1 being Element of L1, q2 being Element of L2 such that

A10: b = [q1,q2] by DOMAIN_1:1;

reconsider q29 = q2 as Element of C2 ;

take q29 ; :: thesis: q29 is_a_complement_of p29

thus q29 is_a_complement_of p29 by A9, A10, Th44; :: thesis: verum