let L1, L2 be Lattice; :: thesis:
let p1, q1 be Element of L1; :: thesis:
let p2, q2 be Element of L2; :: thesis:
assume A0: ( L1 is 01_Lattice & L2 is 01_Lattice ) ; :: thesis:
set L = [:L1,L2:];
thus ( p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 implies [p1,p2] is_a_pseudocomplement_of [q1,q2] ) :: thesis:

proof

assume A1: ( p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 ) ; :: thesis:
set a = [p1,p2];
set b = [q1,q2];
a2: [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A1, FILTER_1:35;
for x being Element of [:L1,L2:] st [q1,q2] "/\" x = Bottom [:L1,L2:] holds
x [= [p1,p2]

proof

let x be Element of [:L1,L2:]; :: thesis:
assume Z1: [q1,q2] "/\" x = Bottom [:L1,L2:] ; :: thesis:
consider x1, x2 being object such that
Z2: ( x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of L1 by Z2;
reconsider x2 = x2 as Element of L2 by Z2;
[q1,q2] "/\" [x1,x2] = [(Bottom L1),(Bottom L2)] by FILTER_1:42, A0, Z2, Z1;
then Z3: [(q1 "/\" x1),(q2 "/\" x2)] = [(Bottom L1),(Bottom L2)] by FILTER_1:35;
then T1: q1 "/\" x1 = Bottom L1 by XTUPLE_0:1;
T2: q2 "/\" x2 = Bottom L2 by Z3, XTUPLE_0:1;
Z4: x1 [= p1 by T1, A1;
x2 [= p2 by A1, T2;
hence x [= [p1,p2] by Z2, FILTER_1:36, Z4; :: thesis:

end;

hence [p1,p2] is_a_pseudocomplement_of [q1,q2] by a2, FILTER_1:42, A0; :: thesis:

end;

assume W0: [p1,p2] is_a_pseudocomplement_of [q1,q2] ; :: thesis:
then [p1,p2] "/\" [q1,q2] = [(Bottom L1),(Bottom L2)] by A0, FILTER_1:42;
then w1: [(p1 "/\" q1),(p2 "/\" q2)] = [(Bottom L1),(Bottom L2)] by FILTER_1:35;
then W1: ( p1 "/\" q1 = Bottom L1 & p2 "/\" q2 = Bottom L2 ) by XTUPLE_0:1;
w2: for xx1 being Element of L1 st q1 "/\" xx1 = Bottom L1 holds
xx1 [= p1

proof

let xx1 be Element of L1; :: thesis:
assume q1 "/\" xx1 = Bottom L1 ; :: thesis:
then [(q1 "/\" xx1),(q2 "/\" p2)] = Bottom [:L1,L2:] by W1, FILTER_1:42, A0;
then [q1,q2] "/\" [xx1,p2] = Bottom [:L1,L2:] by FILTER_1:35;
then [xx1,p2] [= [p1,p2] by W0;
hence xx1 [= p1 by FILTER_1:36; :: thesis:

end;

for xx2 being Element of L2 st q2 "/\" xx2 = Bottom L2 holds
xx2 [= p2

proof

let xx2 be Element of L2; :: thesis:
assume q2 "/\" xx2 = Bottom L2 ; :: thesis:
then [(q1 "/\" p1),(q2 "/\" xx2)] = Bottom [:L1,L2:] by W1, FILTER_1:42, A0;
then [q1,q2] "/\" [p1,xx2] = Bottom [:L1,L2:] by FILTER_1:35;
then [p1,xx2] [= [p1,p2] by W0;
hence xx2 [= p2 by FILTER_1:36; :: thesis:

end;

hence ( p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 ) by w2, w1, XTUPLE_0:1; :: thesis: