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