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)

then
the carrier of (ProjectiveSpace (TOP-REAL 3)) c= conic (0,0,0,0,0,0)
by TARSKI:def 3;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;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

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