theorem Th44:
for
P,
Q being
Element of
BK_model st
P <> Q holds
ex
P1,
P2,
P3,
P4 being
Element of
absolute ex
P5 being
Element of
(ProjectiveSpace (TOP-REAL 3)) st
(
P1 <> P2 &
P,
Q,
P1 are_collinear &
P,
Q,
P2 are_collinear &
P,
P5,
P3 are_collinear &
Q,
P5,
P4 are_collinear &
P1,
P2,
P3 are_mutually_distinct &
P1,
P2,
P4 are_mutually_distinct &
P5 in (tangent P1) /\ (tangent P2) )