take t = the State of S +* (Start-At (l,S)); :: thesis: t is l -started
thus t is l -started ; :: thesis: verum