let LR1, LR2 be strict complete continuous LATTICE; :: thesis:
assume that
A12: the carrier of LR1 = Class (EqRel R) and
A13: for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) and
A14: the carrier of LR2 = Class (EqRel R) and
A15: for x, y being Element of LR2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ; :: thesis:
set cLR2 = the carrier of LR2;
set cLR1 = the carrier of LR1;

assume A16: z in the InternalRel of LR1 ; :: thesis:
then consider x, y being object such that
A17: ( x in the carrier of LR1 & y in the carrier of LR1 ) and
A18: z = [x,y] by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of LR1 by A17;
reconsider x9 = x, y9 = y as Element of LR2 by A12, A14;
x <= y by A16, A18, ORDERS_2:def 5;
then "/\" (x,L) <= "/\" (y,L) by A13;
then x9 <= y9 by A15;
hence z in the InternalRel of LR2 by A18, ORDERS_2:def 5; :: thesis:

end;

assume A19: z in the InternalRel of LR2 ; :: thesis:
then consider x, y being object such that
A20: ( x in the carrier of LR2 & y in the carrier of LR2 ) and
A21: z = [x,y] by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of LR2 by A20;
reconsider x9 = x, y9 = y as Element of LR1 by A12, A14;
x <= y by A19, A21, ORDERS_2:def 5;
then "/\" (x,L) <= "/\" (y,L) by A15;
then x9 <= y9 by A13;
hence z in the InternalRel of LR1 by A21, ORDERS_2:def 5; :: thesis:

end;