let k, n be Nat; :: thesis: ( k - n in Seg k iff n < k )
thus ( k - n in Seg k implies n < k ) :: thesis: ( n < k implies k - n in Seg k )

proof

assume A1: k - n in Seg k ; :: thesis: n < k
then reconsider x = k - n as Element of NAT ;
assume not n < k ; :: thesis: contradiction
then k - n <= n - n by XREAL_1:9;
then x = 0 ;
hence contradiction by A1, FINSEQ_1:1; :: thesis: verum

end;

thus ( n < k implies k - n in Seg k ) by Th12, FINSEQ_1:3; :: thesis: verum