let L1, L2 be Lattice; :: thesis: for p1, q1 being Element of L1
for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
let p1, q1 be Element of L1; :: thesis: for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
let p2, q2 be Element of L2; :: thesis: ( L1 is 01_Lattice & L2 is 01_Lattice implies ( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] ) )
assume A1: ( L1 is 01_Lattice & L2 is 01_Lattice ) ; :: thesis: ( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
thus ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 implies [p1,p2] is_a_complement_of [q1,q2] ) :: thesis: ( [p1,p2] is_a_complement_of [q1,q2] implies ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) )

proof

assume ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) ; :: thesis: [p1,p2] is_a_complement_of [q1,q2]
then A2: ( p1 "\/" q1 = Top L1 & p1 "/\" q1 = Bottom L1 & p2 "\/" q2 = Top L2 & p2 "/\" q2 = Bottom L2 ) by LATTICES:def 18;
hence [p1,p2] "\/" [q1,q2] = [(Top L1),(Top L2)] by Th22
.= Top [:L1,L2:] by A1, Th44 ;
:: according to LATTICES:def 18 :: thesis: ( [q1,q2] "\/" [p1,p2] = Top [:L1,L2:] & [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] & [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] )
hence [q1,q2] "\/" [p1,p2] = Top [:L1,L2:] ; :: thesis: ( [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] & [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] )
thus [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A2, Th22
.= Bottom [:L1,L2:] by A1, Th43 ; :: thesis: [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:]
hence [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] ; :: thesis: verum

end;

assume [p1,p2] is_a_complement_of [q1,q2] ; :: thesis: ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 )
then A3: ( [p1,p2] "\/" [q1,q2] = Top [:L1,L2:] & [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] ) by LATTICES:def 18;
[(Top L1),(Top L2)] = Top [:L1,L2:] by A1, Th44;
then A4: [(Top L1),(Top L2)] = [(p1 "\/" q1),(p2 "\/" q2)] by A3, Th22;
then A5: p1 "\/" q1 = Top L1 by ZFMISC_1:33;
[(Bottom L1),(Bottom L2)] = Bottom [:L1,L2:] by A1, Th43;
then A6: [(p1 "/\" q1),(p2 "/\" q2)] = [(Bottom L1),(Bottom L2)] by A3, Th22;
then p1 "/\" q1 = Bottom L1 by ZFMISC_1:33;
hence p1 is_a_complement_of q1 by A5, LATTICES:def 18; :: thesis: p2 is_a_complement_of q2
A7: p2 "\/" q2 = Top L2 by A4, ZFMISC_1:33;
p2 "/\" q2 = Bottom L2 by A6, ZFMISC_1:33;
hence p2 is_a_complement_of q2 by A7, LATTICES:def 18; :: thesis: verum