let P1, P2 be Point of real_projective_plane; :: thesis: ( ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & P1 = L2P (P,Q) ) & ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & P2 = L2P (P,Q) ) implies P1 = P2 )
assume that
A3: ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & P1 = L2P (P,Q) ) and
A4: ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & P2 = L2P (P,Q) ) ; :: thesis: P1 = P2
consider P, Q being Point of real_projective_plane such that
A5: P <> Q and
A6: l = Line (P,Q) and
A7: P1 = L2P (P,Q) by A3;
consider u, v being non zero Element of (TOP-REAL 3) such that
A8: P = Dir u and
A9: Q = Dir v and
A10: L2P (P,Q) = Dir (u <X> v) by A5, BKMODEL1:def 5;
consider P9, Q9 being Point of real_projective_plane such that
A11: P9 <> Q9 and
A12: l = Line (P9,Q9) and
A13: P2 = L2P (P9,Q9) by A4;
consider u9, v9 being non zero Element of (TOP-REAL 3) such that
A14: P9 = Dir u9 and
A15: Q9 = Dir v9 and
A16: L2P (P9,Q9) = Dir (u9 <X> v9) by A11, BKMODEL1:def 5;
( P,Q,P9 are_collinear & P,Q,Q9 are_collinear ) by A6, A12, COLLSP:10, COLLSP:11;
then ( |{u,v,u9}| = 0 & |{u,v,v9}| = 0 ) by A8, A9, A14, A15, BKMODEL1:1;
then A17: ( |{u9,u,v}| = 0 & |{v9,u,v}| = 0 ) by EUCLID_5:33;
A18: now :: thesis: ( not u <X> v is zero & not u9 <X> v9 is zero )
now :: thesis: not u <X> v = 0. (TOP-REAL 3)
assume u <X> v = 0. (TOP-REAL 3) ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A8, A9, A5, ANPROJ_1:22; :: thesis: verum
end;
hence not u <X> v is zero ; :: thesis: not u9 <X> v9 is zero
now :: thesis: not u9 <X> v9 = 0. (TOP-REAL 3)
assume u9 <X> v9 = 0. (TOP-REAL 3) ; :: thesis: contradiction
then are_Prop u9,v9 by ANPROJ_8:51;
hence contradiction by A14, A15, A11, ANPROJ_1:22; :: thesis: verum
end;
hence not u9 <X> v9 is zero ; :: thesis: verum
end;
then reconsider uv = u <X> v, u9v9 = u9 <X> v9 as non zero Element of (TOP-REAL 3) ;
not are_Prop u9,v9 by A11, A14, A15, ANPROJ_1:22;
then are_Prop uv,u9 <X> v9 by A17, Th8;
hence P1 = P2 by A18, ANPROJ_1:22, A7, A13, A10, A16; :: thesis: verum