set C = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } ;
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } c= the carrier of (ProjectiveSpace (TOP-REAL 3))
proof
let x be
object ;
TARSKI:def 3 ( not x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } or x in the carrier of (ProjectiveSpace (TOP-REAL 3)) )
assume
x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 }
;
x in the carrier of (ProjectiveSpace (TOP-REAL 3))
then
ex
P being
Point of
(ProjectiveSpace (TOP-REAL 3)) st
(
x = P & ( for
u being
Element of
(TOP-REAL 3) st not
u is
zero &
P = Dir u holds
qfconic (
a,
b,
c,
d,
e,
f,
u)
= 0 ) )
;
hence
x in the
carrier of
(ProjectiveSpace (TOP-REAL 3))
;
verum
end;
hence
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } is Subset of (ProjectiveSpace (TOP-REAL 3))
; verum