now 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 ;
( 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))
;
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;
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; verum