let a, b, c, d, e, f be Real; :: thesis: for u being non zero Element of (TOP-REAL 3)
for P being Element of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & qfconic (a,b,c,d,e,f,u) = 0 holds
P in conic (a,b,c,d,e,f)
let u be non zero Element of (TOP-REAL 3); :: thesis: for P being Element of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & qfconic (a,b,c,d,e,f,u) = 0 holds
P in conic (a,b,c,d,e,f)
let P be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P = Dir u & qfconic (a,b,c,d,e,f,u) = 0 implies P in conic (a,b,c,d,e,f) )
assume that
A2: P = Dir u and
A3: qfconic (a,b,c,d,e,f,u) = 0 ; :: thesis: P in conic (a,b,c,d,e,f)
for v being Element of (TOP-REAL 3) st not v is zero & P = Dir v holds
qfconic (a,b,c,d,e,f,v) = 0 by A2, A3, Th10;
hence P in conic (a,b,c,d,e,f) ; :: thesis: verum