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 that
A1: L1 is 01_Lattice and
A2: 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 that
A3: p1 is_a_complement_of q1 and
A4: p2 is_a_complement_of q2 ; :: thesis: [p1,p2] is_a_complement_of [q1,q2]
A5: p2 "\/" q2 = Top L2 by A4, LATTICES:def 18;
p1 "\/" q1 = Top L1 by A3, LATTICES:def 18;
hence [p1,p2] "\/" [q1,q2] = [(Top L1),(Top L2)] by A5, Th22
.= Top [:L1,L2:] by A1, A2, 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:] )
A6: p2 "/\" q2 = Bottom L2 by A4, LATTICES:def 18;
p1 "/\" q1 = Bottom L1 by A3, LATTICES:def 18;
hence [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A6, Th22
.= Bottom [:L1,L2:] by A1, A2, Th43 ;
:: thesis: [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:]
hence [q1,q2] "/\" [p1,p2] = Bottom [:L1,L2:] ; :: thesis: verum

end;

assume A7: [p1,p2] is_a_complement_of [q1,q2] ; :: thesis: ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 )
then A8: [p1,p2] "/\" [q1,q2] = Bottom [:L1,L2:] by LATTICES:def 18;
[(Bottom L1),(Bottom L2)] = Bottom [:L1,L2:] by A1, A2, Th43;
then A9: [(p1 "/\" q1),(p2 "/\" q2)] = [(Bottom L1),(Bottom L2)] by A8, Th22;
then A10: p1 "/\" q1 = Bottom L1 by ZFMISC_1:33;
A11: [p1,p2] "\/" [q1,q2] = Top [:L1,L2:] by A7, LATTICES:def 18;
A12: p2 "/\" q2 = Bottom L2 by A9, ZFMISC_1:33;
[(Top L1),(Top L2)] = Top [:L1,L2:] by A1, A2, Th44;
then A13: [(Top L1),(Top L2)] = [(p1 "\/" q1),(p2 "\/" q2)] by A11, Th22;
then p1 "\/" q1 = Top L1 by ZFMISC_1:33;
hence p1 is_a_complement_of q1 by A10, LATTICES:def 18; :: thesis: p2 is_a_complement_of q2
p2 "\/" q2 = Top L2 by A13, ZFMISC_1:33;
hence p2 is_a_complement_of q2 by A12, LATTICES:def 18; :: thesis: verum