take Start-At (0,S) ; :: thesis: not Start-At (0,S) is empty
thus not Start-At (0,S) is empty ; :: thesis: verum