theorem Th31: :: SCMRING3:32

for R being Ring
for a being Data-Location of R
for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )