R.<t, u_,v_,w_, u,v,w, x,y,z> = QQ[]

# aim: verify automatically that x^2 + y^2 - z^2 = -1 is composed of lines.

p = x^2 + y^2 - z^2 + 1

line = vector((x, y, z)) + t*vector((u, v, w))

# for all x,y,z if p(x,y,z) = 0 then
# there are u,v,w not all zero such that
# for all t, p(line) = 0

p_line = p(x=line[0], y=line[1], z=line[2])
line_included = forall_t_p_line = p_line.polynomial(t).coefficients()

uvw_nonzero = u*u_ + v*v_ + w*w_ + 1
uvw_condition = ideal(line_included + [uvw_nonzero])

there_are_uvw = uvw_condition.elimination_ideal([u,v,w,u_,v_,w_])

assert there_are_uvw == ideal(p), "p does not appear to be composed of lines!"

print('OK')