let P1, P2 be Point of real_projective_plane; :: thesis: ( ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & P1 = Dir (u <X> v) ) & ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & P2 = Dir (u <X> v) ) implies P1 = P2 )
assume that
A4: ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & P1 = Dir (u <X> v) ) and
A5: ex u, v being non zero Element of (TOP-REAL 3) st
( p = Dir u & q = Dir v & P2 = Dir (u <X> v) ) ; :: thesis: P1 = P2
consider u1, v1 being non zero Element of (TOP-REAL 3) such that
A6: ( p = Dir u1 & q = Dir v1 & P1 = Dir (u1 <X> v1) ) by A4;
consider u2, v2 being non zero Element of (TOP-REAL 3) such that
A7: ( p = Dir u2 & q = Dir v2 & P2 = Dir (u2 <X> v2) ) by A5;
A8: ( not u1 <X> v1 is zero & not u2 <X> v2 is zero ) by A1, A6, A7, Th64;
A9: ( are_Prop u1,u2 & are_Prop v1,v2 ) by A6, A7, ANPROJ_1:22;
then consider a being Real such that
A10: ( a <> 0 & u1 = a * u2 ) by ANPROJ_1:1;
consider b being Real such that
A11: ( b <> 0 & v1 = b * v2 ) by A9, ANPROJ_1:1;
u1 <X> v1 = (b * (a * u2)) <X> v2 by A10, A11, EUCLID_5:16
.= ((a * b) * u2) <X> v2 by RVSUM_1:49
.= (a * b) * (u2 <X> v2) by EUCLID_5:16 ;
then are_Prop u1 <X> v1,u2 <X> v2 by A10, A11, ANPROJ_1:1;
hence P1 = P2 by A6, A7, A8, ANPROJ_1:22; :: thesis: verum