theorem Th07: :: BKMODEL2:13

for L being LINE of (IncProjSp_of real_projective_plane)
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in L & Q in L holds
L = Line (P,Q)