take s = the State of S +* (Start-At (l,S)); :: thesis: s is l -started
thus IC in dom s by Lm6; :: according to MEMSTR_0:def 8 :: thesis: IC s = l
thus IC s = l by Lm142; :: thesis: verum