theorem Th4: :: SCMPDS_9:4

for a being Int_position
for l being Element of NAT holds NIC ((return a),l) = { k where k is Nat : k > 1 }