let P be Element of absolute ; :: thesis: P <> pole_infty P
assume A1: P = pole_infty P ; :: thesis: contradiction
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & pole_infty P = Dir |[(- (u . 2)),(u . 1),0]| ) by Def03;
A3: not |[(- (u . 2)),(u . 1),0]| is zero by A2, BKMODEL1:91;
are_Prop u,|[(- (u . 2)),(u . 1),0]| by A1, A2, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A4: u = a * |[(- (u . 2)),(u . 1),0]| by ANPROJ_1:1;
1 = a * (|[(- (u . 2)),(u . 1),0]| . 3) by A2, A4, RVSUM_1:44
.= a * (|[(- (u . 2)),(u . 1),0]| `3) by EUCLID_5:def 3
.= a * 0 by EUCLID_5:2
.= 0 ;
hence contradiction ; :: thesis: verum