theorem :: JORDAN12:1

for i being Nat st 1 < i holds
0 < i -' 1