let P, Q, R be non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P,Q,R are_collinear iff Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R )
reconsider p = RP3_to_T2 P, q = RP3_to_T2 Q, r = RP3_to_T2 R as POINT of TarskiEuclid2Space ;
consider u being non zero Element of (TOP-REAL 3) such that
A1: ( P = Dir u & u `3 = 1 & RP3_to_REAL2 P = |[(u `1),(u `2)]| ) by Def05;
consider v being non zero Element of (TOP-REAL 3) such that
A2: ( Q = Dir v & v `3 = 1 & RP3_to_REAL2 Q = |[(v `1),(v `2)]| ) by Def05;
consider w being non zero Element of (TOP-REAL 3) such that
A3: ( R = Dir w & w `3 = 1 & RP3_to_REAL2 R = |[(w `1),(w `2)]| ) by Def05;

hereby :: thesis: ( Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R implies P,Q,R are_collinear )

assume A4: P,Q,R are_collinear ; :: thesis: Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R
u,v,w are_collinear by A4, A1, A2, A3, Th43;

per cases then ( u in LSeg (v,w) or v in LSeg (w,u) or w in LSeg (u,v) ) by TOPREAL9:67;

suppose u in LSeg (v,w) ; :: thesis: Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R

then Tn2TR p in LSeg ((Tn2TR q),(Tn2TR r)) by A1, A2, A3, Th44;
hence Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R by GTARSKI2:20; :: thesis: verum

end;

suppose v in LSeg (w,u) ; :: thesis: Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R

then Tn2TR q in LSeg ((Tn2TR r),(Tn2TR p)) by A1, A2, A3, Th44;
hence Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R by GTARSKI2:20; :: thesis: verum

end;

suppose w in LSeg (u,v) ; :: thesis: Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R

then Tn2TR r in LSeg ((Tn2TR p),(Tn2TR q)) by A1, A2, A3, Th44;
hence Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R by GTARSKI2:20; :: thesis: verum

end;

end;

end;

assume Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R ; :: thesis: P,Q,R are_collinear
then A5: ( Tn2TR q in LSeg ((Tn2TR p),(Tn2TR r)) or Tn2TR r in LSeg ((Tn2TR q),(Tn2TR p)) or Tn2TR p in LSeg ((Tn2TR r),(Tn2TR q)) ) by GTARSKI2:20;
reconsider u1 = Tn2TR p, v1 = Tn2TR q, w1 = Tn2TR r as Element of (TOP-REAL 2) ;
reconsider u9 = |[(u1 `1),(u1 `2),1]|, v9 = |[(v1 `1),(v1 `2),1]|, w9 = |[(w1 `1),(w1 `2),1]| as Element of (TOP-REAL 3) ;

now :: thesis: ( Dir u9 = P & Dir v9 = Q & Dir w9 = R & u9 `3 = 1 & v9 `3 = 1 & w9 `3 = 1 & u9,v9,w9 are_collinear )

( u1 `1 = u `1 & u1 `2 = u `2 & v1 `1 = v `1 & v1 `2 = v `2 & w1 `1 = w `1 & w1 `2 = w `2 ) by A1, A2, A3, EUCLID:52;
hence ( Dir u9 = P & Dir v9 = Q & Dir w9 = R ) by A1, A2, A3, EUCLID_5:3; :: thesis: ( u9 `3 = 1 & v9 `3 = 1 & w9 `3 = 1 & u9,v9,w9 are_collinear )
thus ( u9 `3 = 1 & v9 `3 = 1 & w9 `3 = 1 ) by EUCLID_5:2; :: thesis: u9,v9,w9 are_collinear
( v9 in LSeg (u9,w9) or w9 in LSeg (v9,u9) or u9 in LSeg (w9,v9) ) by A5, Th45;
hence u9,v9,w9 are_collinear by TOPREAL9:67; :: thesis: verum

end;

hence P,Q,R are_collinear by Th43; :: thesis: verum