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