let P, Q be Element of BK_model ; ( P <> Q implies ex R being Element of absolute st
for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = P & q = Q & r = R holds
between RP3_to_T2 q, RP3_to_T2 p, RP3_to_T2 r )
assume A1:
P <> Q
; ex R being Element of absolute st
for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = P & q = Q & r = R holds
between RP3_to_T2 q, RP3_to_T2 p, RP3_to_T2 r
then consider P1, P2 being Element of absolute such that
A2:
P1 <> P2
and
A3:
( P,Q,P1 are_collinear & P,Q,P2 are_collinear )
by BKMODEL2:20;
reconsider p = P, q = Q, p1 = P1, p2 = P2 as Element of (ProjectiveSpace (TOP-REAL 3)) ;
now ( not p is point_at_infty & not q is point_at_infty & not p1 is point_at_infty & not p2 is point_at_infty )consider u being
Element of
(TOP-REAL 3) such that A4:
not
u is
zero
and A5:
p = Dir u
by ANPROJ_1:26;
u . 3
<> 0
by A4, A5, BKMODEL2:2;
then
u `3 <> 0
by EUCLID_5:def 3;
hence
not
p is
point_at_infty
by A4, A5, Th40;
( not q is point_at_infty & not p1 is point_at_infty & not p2 is point_at_infty )consider v being
Element of
(TOP-REAL 3) such that A6:
not
v is
zero
and A7:
q = Dir v
by ANPROJ_1:26;
v . 3
<> 0
by A6, A7, BKMODEL2:2;
then
v `3 <> 0
by EUCLID_5:def 3;
hence
not
q is
point_at_infty
by A6, A7, Th40;
( not p1 is point_at_infty & not p2 is point_at_infty )consider w being non
zero Element of
(TOP-REAL 3) such that A8:
w . 3
= 1
and A9:
p1 = Dir w
by BKMODEL3:30;
w `3 <> 0
by A8, EUCLID_5:def 3;
hence
not
p1 is
point_at_infty
by A9, Th40;
not p2 is point_at_infty consider x being non
zero Element of
(TOP-REAL 3) such that A10:
x . 3
= 1
and A11:
p2 = Dir x
by BKMODEL3:30;
x `3 <> 0
by A10, EUCLID_5:def 3;
hence
not
p2 is
point_at_infty
by A11, Th40;
verum end;
then reconsider p = p, q = q, p1 = p1, p2 = p2 as non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) ;