take Start-At l,S ; :: thesis: Start-At l,S is l -started
thus Start-At l,S is l -started ; :: thesis: verum