let P1, P2 be Element of real_projective_plane; :: thesis: ( ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & P1 = Dir |[(- (u . 2)),(u . 1),0]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & P2 = Dir |[(- (u . 2)),(u . 1),0]| ) implies P1 = P2 )
assume that
A4: ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & P1 = Dir |[(- (u . 2)),(u . 1),0]| ) and
A5: ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & P2 = Dir |[(- (u . 2)),(u . 1),0]| ) ; :: thesis: P1 = P2
consider u1 being non zero Element of (TOP-REAL 3) such that
A6: ( P = Dir u1 & u1 . 3 = 1 & ((u1 . 1) ^2) + ((u1 . 2) ^2) = 1 & P1 = Dir |[(- (u1 . 2)),(u1 . 1),0]| ) by A4;
consider u2 being non zero Element of (TOP-REAL 3) such that
A7: ( P = Dir u2 & u2 . 3 = 1 & ((u2 . 1) ^2) + ((u2 . 2) ^2) = 1 & P2 = Dir |[(- (u2 . 2)),(u2 . 1),0]| ) by A5;
A8: not |[(- (u2 . 2)),(u2 . 1),0]| is zero by A7, BKMODEL1:91;
A9: not |[(- (u1 . 2)),(u1 . 1),0]| is zero by A6, BKMODEL1:91;
are_Prop u1,u2 by A6, A7, ANPROJ_1:22;
then consider a being Real such that
A10: a <> 0 and
A11: u2 = a * u1 by ANPROJ_1:1;
A12: - (u2 . 2) = - (a * (u1 . 2)) by A11, RVSUM_1:44
.= a * (- (u1 . 2)) ;
|[(- (u2 . 2)),(u2 . 1),0]| = |[(a * (- (u1 . 2))),(a * (u1 . 1)),(a * 0)]| by A11, RVSUM_1:44, A12
.= a * |[(- (u1 . 2)),(u1 . 1),0]| by EUCLID_5:8 ;
then are_Prop |[(- (u2 . 2)),(u2 . 1),0]|,|[(- (u1 . 2)),(u1 . 1),0]| by A10, ANPROJ_1:1;
hence P1 = P2 by A8, A9, A6, A7, ANPROJ_1:22; :: thesis: verum