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