thus ( s is l -started implies IC s = l ) by Def41; :: thesis: ( IC s = l implies s is l -started )
assume Z: IC s = l ; :: thesis: s is l -started
thus IC S in dom s by L94; :: according to COMPOS_1:def 16 :: thesis: IC s = l
thus IC s = l by Z; :: thesis: verum