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

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

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 A7:
[p1,p2] is_a_complement_of [q1,q2]
; :: thesis: ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 )
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;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

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