dom (Start-At (l,S)) = {(IC )} by FUNCOP_1:13;
hence IC in dom (Start-At (l,S)) by TARSKI:def 1; :: according to MEMSTR_0:def 11 :: thesis: ( IC (Start-At (l,S)) = l & not Start-At (l,S) is empty )
thus ( IC (Start-At (l,S)) = l & not Start-At (l,S) is empty ) by FUNCOP_1:72; :: thesis: verum