let n1, n2 be Element of NAT ; :: thesis:

assume that
A5: ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n1 = n ! ) and
A6: ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n2 = n ! ) ; :: thesis:
consider n being Element of NAT such that
A7: n ! <= x and
A8: x < (n + 1) ! and
A9: n1 = n ! by A5;
consider m being Element of NAT such that
A10: m ! <= x and
A11: x < (m + 1) ! and
A12: n2 = m ! by A6;

assume A13: m <> n ; :: thesis:
thus contradiction :: thesis:

proof

per cases by A13, XXREAL_0:1;

suppose m > n ; :: thesis:

then m >= n + 1 by INT_1:7;
then m ! >= (n + 1) ! by Lm51;
hence contradiction by A8, A10, XXREAL_0:2; :: thesis:

end;

suppose m < n ; :: thesis:

then m + 1 <= n by INT_1:7;
then (m + 1) ! <= n ! by Lm51;
hence contradiction by A7, A11, XXREAL_0:2; :: thesis:

end;

hence n1 = n2 by A9, A12; :: thesis:

end;

hence ( ( x <> 0 & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n1 = n ! ) & ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & n2 = n ! ) implies n1 = n2 ) & ( not x <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ) ; :: thesis: