let L1, L2 be Lattice; :: thesis:
set R = LattRel [:L1,L2:];
set S = LattRel [:L2,L1:];
set D1 = the carrier of L1;
set D2 = the carrier of L2;
set p2 = pr2 ( the carrier of L1, the carrier of L2);
set p1 = pr1 ( the carrier of L1, the carrier of L2);
take f = <:(pr2 ( the carrier of L1, the carrier of L2)),(pr1 ( the carrier of L1, the carrier of L2)):>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis:
A1: dom (pr2 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 5;
A2: field (LattRel [:L1,L2:]) = the carrier of [:L1,L2:] by Th32;
A3: rng (pr2 ( the carrier of L1, the carrier of L2)) = the carrier of L2 by FUNCT_3:46;
A4: field (LattRel [:L2,L1:]) = the carrier of [:L2,L1:] by Th32;
dom (pr1 ( the carrier of L1, the carrier of L2)) = [: the carrier of L1, the carrier of L2:] by FUNCT_3:def 4;
then (dom (pr2 ( the carrier of L1, the carrier of L2))) /\ (dom (pr1 ( the carrier of L1, the carrier of L2))) = [: the carrier of L1, the carrier of L2:] by A1;
hence A5: dom f = field (LattRel [:L1,L2:]) by A2, FUNCT_3:def 7; :: according to WELLORD1:def 7 :: thesis:
rng (pr1 ( the carrier of L1, the carrier of L2)) = the carrier of L1 by FUNCT_3:44;
hence rng f c= field (LattRel [:L2,L1:]) by A4, A3, FUNCT_3:51; :: according to XBOOLE_0:def 10 :: thesis:
thus field (LattRel [:L2,L1:]) c= rng f :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in field (LattRel [:L2,L1:]) ; :: thesis:
then consider r2 being Element of L2, r1 being Element of L1 such that
A6: x = [r2,r1] by A4, DOMAIN_1:1;
A7: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;
A8: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;
f . [r1,r2] in rng f by A2, A5, FUNCT_1:def 3;
hence x in rng f by A2, A5, A6, A7, A8, FUNCT_3:def 7; :: thesis:

end;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume A9: x in dom f ; :: thesis:
then A10: f . x = [((pr2 ( the carrier of L1, the carrier of L2)) . x),((pr1 ( the carrier of L1, the carrier of L2)) . x)] by FUNCT_3:def 7;
consider r1 being Element of L1, r2 being Element of L2 such that
A11: x = [r1,r2] by A2, A5, A9, DOMAIN_1:1;
A12: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;
A13: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;
assume that
A14: y in dom f and
A15: f . x = f . y ; :: thesis:
A16: f . y = [((pr2 ( the carrier of L1, the carrier of L2)) . y),((pr1 ( the carrier of L1, the carrier of L2)) . y)] by A14, FUNCT_3:def 7;
consider q1 being Element of L1, q2 being Element of L2 such that
A17: y = [q1,q2] by A2, A5, A14, DOMAIN_1:1;
A18: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;
(pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;
then r1 = q1 by A11, A15, A17, A13, A10, A16, XTUPLE_0:1;
hence x = y by A11, A15, A17, A12, A18, A10, A16, XTUPLE_0:1; :: thesis:

end;

let x, y be object ; :: thesis:
thus ( [x,y] in LattRel [:L1,L2:] implies ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) :: thesis:

assume [x,y] in LattRel [:L1,L2:] ; :: thesis:
then consider a, b being Element of [:L1,L2:] such that
A19: [x,y] = [a,b] and
A20: a [= b ;
consider q1 being Element of L1, q2 being Element of L2 such that
A21: b = [q1,q2] by DOMAIN_1:1;
A22: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A21, FUNCT_3:def 7;
A23: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;
consider r1 being Element of L1, r2 being Element of L2 such that
A24: a = [r1,r2] by DOMAIN_1:1;
A25: r2 [= q2 by A20, A24, A21, Th36;
r1 [= q1 by A20, A24, A21, Th36;
then A26: [r2,r1] [= [q2,q1] by A25, Th36;
A27: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;
A28: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;
A29: y = b by A19, XTUPLE_0:1;
A30: x = a by A19, XTUPLE_0:1;
hence ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) ) by A2, A29; :: thesis:
A31: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;
f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A24, FUNCT_3:def 7;
hence [(f . x),(f . y)] in LattRel [:L2,L1:] by A24, A21, A30, A29, A26, A27, A28, A31, A23, A22; :: thesis:

end;

assume that
A32: x in field (LattRel [:L1,L2:]) and
A33: y in field (LattRel [:L1,L2:]) ; :: thesis:
consider q1 being Element of L1, q2 being Element of L2 such that
A34: y = [q1,q2] by A2, A33, DOMAIN_1:1;
A35: f . (q1,q2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2)),((pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2))] by A2, A5, A34, FUNCT_3:def 7;
assume A36: [(f . x),(f . y)] in LattRel [:L2,L1:] ; :: thesis:
A37: (pr2 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q2 by FUNCT_3:def 5;
A38: (pr1 ( the carrier of L1, the carrier of L2)) . (q1,q2) = q1 by FUNCT_3:def 4;
consider r1 being Element of L1, r2 being Element of L2 such that
A39: x = [r1,r2] by A2, A32, DOMAIN_1:1;
A40: (pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r2 by FUNCT_3:def 5;
A41: (pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2) = r1 by FUNCT_3:def 4;
f . (r1,r2) = [((pr2 ( the carrier of L1, the carrier of L2)) . (r1,r2)),((pr1 ( the carrier of L1, the carrier of L2)) . (r1,r2))] by A2, A5, A39, FUNCT_3:def 7;
then A42: [r2,r1] [= [q2,q1] by A39, A34, A36, A41, A40, A35, A38, A37, Th31;
then A43: r1 [= q1 by Th36;
r2 [= q2 by A42, Th36;
then [r1,r2] [= [q1,q2] by A43, Th36;
hence [x,y] in LattRel [:L1,L2:] by A39, A34; :: thesis: