let P1, P2 be Element of absolute ; :: thesis: ( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
assume A1: pole_infty P1 = pole_infty P2 ; :: thesis: ( P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
consider u1 being non zero Element of (TOP-REAL 3) such that
A2: ( P1 = Dir u1 & u1 . 3 = 1 & ((u1 . 1) ^2) + ((u1 . 2) ^2) = 1 & pole_infty P1 = Dir |[(- (u1 . 2)),(u1 . 1),0]| ) by Def03;
consider u2 being non zero Element of (TOP-REAL 3) such that
A3: ( P2 = Dir u2 & u2 . 3 = 1 & ((u2 . 1) ^2) + ((u2 . 2) ^2) = 1 & pole_infty P2 = Dir |[(- (u2 . 2)),(u2 . 1),0]| ) by Def03;
reconsider w1 = |[(- (u1 . 2)),(u1 . 1),0]| as non zero Element of (TOP-REAL 3) by A2, BKMODEL1:91;
reconsider w2 = |[(- (u2 . 2)),(u2 . 1),0]| as non zero Element of (TOP-REAL 3) by A3, BKMODEL1:91;
are_Prop w1,w2 by A1, A2, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A5: w1 = a * w2 by ANPROJ_1:1;
a * w2 = |[(a * (- (u2 . 2))),(a * (u2 . 1)),(a * 0)]| by EUCLID_5:8;
then A6: ( - (u1 . 2) = a * (- (u2 . 2)) & u1 . 1 = a * (u2 . 1) ) by A5, FINSEQ_1:78;
then A7: 1 = ((a * (u2 . 1)) * (a * (u2 . 1))) + ((a * (u2 . 2)) ^2) by A2
.= (a * a) * (((u2 . 1) * (u2 . 1)) + ((u2 . 2) * (u2 . 2)))
.= a ^2 by A3 ;
A8: ( a = 1 implies P1 = P2 )

proof

assume a = 1 ; :: thesis: P1 = P2
then ( u1 `1 = u2 . 1 & u1 `2 = u2 . 2 & u1 `3 = u2 . 3 ) by A2, A3, A6, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A9: ( u1 `1 = u2 `1 & u1 `2 = u2 `2 & u1 `3 = u2 `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u1 = |[(u1 `1),(u1 `2),(u1 `3)]| by EUCLID_5:3
.= u2 by A9, EUCLID_5:3 ;
hence P1 = P2 by A2, A3; :: thesis: verum

end;

( a = - 1 implies ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )

proof

assume a = - 1 ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 )
then ( u1 `1 = - (u2 . 1) & u1 `2 = - (u2 . 2) & u2 `3 = 1 ) by A3, A6, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A10: ( u1 `1 = - (u2 `1) & u1 `2 = - (u2 `2) & u2 `3 = 1 ) by EUCLID_5:def 1, EUCLID_5:def 2;
take u1 ; :: thesis: ( P1 = Dir u1 & P2 = Dir |[(- (u1 `1)),(- (u1 `2)),1]| & u1 `3 = 1 )
thus ( P1 = Dir u1 & P2 = Dir |[(- (u1 `1)),(- (u1 `2)),1]| & u1 `3 = 1 ) by A10, EUCLID_5:3, A3, A2, EUCLID_5:def 3; :: thesis: verum

end;

hence ( P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) ) by A7, A8, SQUARE_1:41; :: thesis: verum