let n be Element of NAT ; :: thesis: ( n >= 1 implies ((n ^2) - n) + 1 <= n ^2 )
assume A1: n >= 1 ; :: thesis: ((n ^2) - n) + 1 <= n ^2

now :: thesis: not ((n ^2) - n) + 1 > n ^2

assume ((n ^2) - n) + 1 > n ^2 ; :: thesis: contradiction
then (- (n ^2)) + ((n ^2) + ((- n) + 1)) > (n ^2) + (- (n ^2)) by XREAL_1:6;
then 1 > 0 - (- n) by XREAL_1:19;
hence contradiction by A1; :: thesis: verum

end;

hence ((n ^2) - n) + 1 <= n ^2 ; :: thesis: verum