thus ( s is l -started implies IC s = l ) by Def16; :: thesis: ( IC s = l implies s is l -started )
assume A1: IC s = l ; :: 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 A1; :: thesis: verum