divisors (n,m,r) c= Segm (n + 1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in divisors (n,m,r) or x in Segm (n + 1) )
assume A1: x in divisors (n,m,r) ; :: thesis: x in Segm (n + 1)
then reconsider x = x as Nat ;
x <= n by A1, Th12, NAT_D:7;
then x < n + 1 by NAT_1:13;
hence x in Segm (n + 1) by NAT_1:44; :: thesis: verum

end;

hence divisors (n,m,r) is finite ; :: thesis: verum