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;
p1 "\/" q1 = Top L1 by A3;
hence [p1,p2] "\/" [q1,q2] = [(Top L1),(Top L2)] by A5, Th21
.= Top [:L1,L2:] by A1, A2, Th43 ;
:: 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;
p1 "/\" q1 = Bottom L1 by A3;
hence [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A6, Th21
.= Bottom [:L1,L2:] by A1, A2, Th42 ;
:: 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:] ;
[(Bottom L1),(Bottom L2)] = Bottom [:L1,L2:] by A1, A2, Th42;
then A9: [(p1 "/\" q1),(p2 "/\" q2)] = [(Bottom L1),(Bottom L2)] by A8, Th21;
then A10: p1 "/\" q1 = Bottom L1 by XTUPLE_0:1;
A11: [p1,p2] "\/" [q1,q2] = Top [:L1,L2:] by A7;
A12: p2 "/\" q2 = Bottom L2 by A9, XTUPLE_0:1;
A13: ( p1 "\/" q1 = q1 "\/" p1 & p1 "/\" q1 = q1 "/\" p1 ) ;
[(Top L1),(Top L2)] = Top [:L1,L2:] by A1, A2, Th43;
then A14: [(Top L1),(Top L2)] = [(p1 "\/" q1),(p2 "\/" q2)] by A11, Th21;
then p1 "\/" q1 = Top L1 by XTUPLE_0:1;
hence p1 is_a_complement_of q1 by A10, A13; :: thesis: p2 is_a_complement_of q2
A15: ( p2 "\/" q2 = q2 "\/" p2 & p2 "/\" q2 = q2 "/\" p2 ) ;
p2 "\/" q2 = Top L2 by A14, XTUPLE_0:1;
hence p2 is_a_complement_of q2 by A12, A15; :: thesis: verum