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, Th41;
L is complemented
proof
let a be Element of L; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of L st b1 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;
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 Th41;
C1 is complemented
proof
set p29 = the Element of C2;
let p19 be Element of C1; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of C1 st b1 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;
hence L1 is C_Lattice ; :: thesis: L2 is C_Lattice
C2 is complemented
proof
set p19 = the Element of C1;
let p29 be Element of C2; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of C2 st b1 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;
hence L2 is C_Lattice ; :: thesis: verum