now :: thesis: for o being object st o in the carrier of (ProjectiveSpace (TOP-REAL 3)) holds
o in conic (0,0,0,0,0,0)

let o be object ; :: thesis: ( o in the carrier of (ProjectiveSpace (TOP-REAL 3)) implies o in conic (0,0,0,0,0,0) )
assume A1: o in the carrier of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: o in conic (0,0,0,0,0,0)
for u being Element of (TOP-REAL 3) st not u is zero & o = Dir u holds
qfconic (0,0,0,0,0,0,u) = 0 ;
hence o in conic (0,0,0,0,0,0) by A1; :: thesis: verum

end;

then the carrier of (ProjectiveSpace (TOP-REAL 3)) c= conic (0,0,0,0,0,0) by TARSKI:def 3;
hence conic (0,0,0,0,0,0) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by XBOOLE_0:def 10; :: thesis: verum