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