let n, m, k be Nat; :: thesis: ( k in primeNumbers (n,m) iff ( n < k & k <= n + m & k is prime ) )
thus ( k in primeNumbers (n,m) implies ( n < k & k <= n + m & k is prime ) ) :: thesis: ( n < k & k <= n + m & k is prime implies k in primeNumbers (n,m) )

proof

assume k in primeNumbers (n,m) ; :: thesis: ( n < k & k <= n + m & k is prime )
then k in (seq (n,m)) /\ SetPrimes by NUMBER14:def 17;
hence ( n < k & k <= n + m & k is prime ) by Th73, NEWTON:def 6; :: thesis: verum

end;

assume ( n < k & k <= n + m & k is prime ) ; :: thesis: k in primeNumbers (n,m)
then ( k in seq (n,m) & k in SetPrimes ) by Th73, NEWTON:def 6;
then k in (seq (n,m)) /\ SetPrimes by XBOOLE_0:def 4;
hence k in primeNumbers (n,m) by NUMBER14:def 17; :: thesis: verum