theorem Th15: :: AMI_8:15

for i1, i2, i3 being Integer
for s being State of SCM st Initialize (((dl. 0),(dl. 1),(dl. 2)) --> (i1,i2,i3)) c= s holds
s is State-consisting of <%i1,i2,i3%>