let L1, L2 be Lattice; :: thesis: [:L1,L2:],[:L2,L1:] are_isomorphic
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: f is_isomorphism_of LattRel [:L1,L2:], LattRel [:L2,L1:]
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 ; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:L2,L1:]) & f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )

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 ; :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:L2,L1:]) c= rng f & f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )

thus field (LattRel [:L2,L1:]) c= rng f :: thesis: ( f is one-to-one & ( for b1, b2 being object holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field (LattRel [:L2,L1:]) or x in rng f )
assume x in field (LattRel [:L2,L1:]) ; :: thesis: x in rng f
then consider r2 being Element of L2, r1 being Element of L1 such that
A6: x = [r2,r1] by ;
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 ;
hence x in rng f by ; :: thesis: verum
end;
thus f is one-to-one :: thesis: for b1, b2 being object holds
( ( not [b1,b2] in LattRel [:L1,L2:] or ( b1 in field (LattRel [:L1,L2:]) & b2 in field (LattRel [:L1,L2:]) & [(f . b1),(f . b2)] in LattRel [:L2,L1:] ) ) & ( not b1 in field (LattRel [:L1,L2:]) or not b2 in field (LattRel [:L1,L2:]) or not [(f . b1),(f . b2)] in LattRel [:L2,L1:] or [b1,b2] in LattRel [:L1,L2:] ) )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A9: x in dom f ; :: thesis: ( not y in dom f or not f . x = f . y or x = y )
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 ;
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: x = y
A16: f . y = [((pr2 ( the carrier of L1, the carrier of L2)) . y),((pr1 ( the carrier of L1, the carrier of L2)) . y)] by ;
consider q1 being Element of L1, q2 being Element of L2 such that
A17: y = [q1,q2] by ;
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 ;
hence x = y by ; :: thesis: verum
end;
let x, y be object ; :: thesis: ( ( not [x,y] in LattRel [:L1,L2:] or ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] ) ) & ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] ) )
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: ( not x in field (LattRel [:L1,L2:]) or not y in field (LattRel [:L1,L2:]) or not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )
proof
assume [x,y] in LattRel [:L1,L2:] ; :: thesis: ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) & [(f . x),(f . y)] in LattRel [:L2,L1:] )
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 ;
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 ;
r1 [= q1 by ;
then A26: [r2,r1] [= [q2,q1] by ;
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 ;
A30: x = a by ;
hence ( x in field (LattRel [:L1,L2:]) & y in field (LattRel [:L1,L2:]) ) by ; :: thesis: [(f . x),(f . y)] in LattRel [:L2,L1:]
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 ;
hence [(f . x),(f . y)] in LattRel [:L2,L1:] by A24, A21, A30, A29, A26, A27, A28, A31, A23, A22; :: thesis: verum
end;
assume that
A32: x in field (LattRel [:L1,L2:]) and
A33: y in field (LattRel [:L1,L2:]) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:L2,L1:] or [x,y] in LattRel [:L1,L2:] )
consider q1 being Element of L1, q2 being Element of L2 such that
A34: y = [q1,q2] by ;
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 ;
assume A36: [(f . x),(f . y)] in LattRel [:L2,L1:] ; :: thesis: [x,y] in LattRel [:L1,L2:]
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 ;
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 ;
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 ;
then [r1,r2] [= [q1,q2] by ;
hence [x,y] in LattRel [:L1,L2:] by ; :: thesis: verum