let x, y be Element of NAT ; :: thesis: ( x solves_CRT a1,n1,a2,n2 & x < n1 * n2 & y solves_CRT a1,n1,a2,n2 & y < n1 * n2 implies x = y )
assume that
A5: x solves_CRT a1,n1,a2,n2 and
A6: x < n1 * n2 and
A7: y solves_CRT a1,n1,a2,n2 and
A8: y < n1 * n2 ; :: thesis: x = y
A9: x,x are_congruent_mod n1 * n2 by INT_1:11;
assume x <> y ; :: thesis: contradiction

per cases then ( x > y or x < y ) by XXREAL_0:1;

suppose A10: x > y ; :: thesis: contradiction

then A11: x - y is Element of NAT by INT_1:5;
A12: x - y,a1 - a1 are_congruent_mod n1 by A5, A7, INT_1:17;
x - y,a2 - a2 are_congruent_mod n2 by A5, A7, INT_1:17;
then x,y are_congruent_mod n1 * n2 by A1, A11, A12, PEPIN:4;
hence contradiction by A6, A8, A9, A10, NAT_6:14; :: thesis: verum

end;

suppose A13: x < y ; :: thesis: contradiction

then A14: y - x is Element of NAT by INT_1:5;
A15: y - x,a1 - a1 are_congruent_mod n1 by A5, A7, INT_1:17;
y - x,a2 - a2 are_congruent_mod n2 by A5, A7, INT_1:17;
then y,x are_congruent_mod n1 * n2 by A1, A14, A15, PEPIN:4;
then x,y are_congruent_mod n1 * n2 by INT_1:14;
hence contradiction by A6, A8, A9, A13, NAT_6:14; :: thesis: verum

end;

end;