theorem :: PAPPUS:20

conic (0,0,0,0,0,0) = the carrier of (ProjectiveSpace (TOP-REAL 3))