let P be non zero_proj1 non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: dual1 P = dual2 P
consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: P = Dir u by ANPROJ_1:26;
reconsider u = u as non zero Element of (TOP-REAL 3) by A1;
A3: ( normalize_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| & normalize_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]| ) by A2, Th11, Th14;

now :: thesis: ( Line ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir2a P),(Pdir2b P)) & Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir1a P),(Pdir1b P)) )

now :: thesis: for x being object st x in Line ((Pdir1a P),(Pdir1b P)) holds
x in Line ((Pdir2a P),(Pdir2b P))

let x be object ; :: thesis: ( x in Line ((Pdir1a P),(Pdir1b P)) implies x in Line ((Pdir2a P),(Pdir2b P)) )
assume x in Line ((Pdir1a P),(Pdir1b P)) ; :: thesis: x in Line ((Pdir2a P),(Pdir2b P))
then consider P9 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A4: x = P9 and
A5: Pdir1a P, Pdir1b P,P9 are_collinear ;
consider u9 being Element of (TOP-REAL 3) such that
A6: not u9 is zero and
A7: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - ((normalize_proj1 P) . 2);
set a3 = - ((normalize_proj1 P) . 3);
set b1 = u9 `1 ;
set b2 = u9 `2 ;
set b3 = u9 `3 ;
A8: - ((normalize_proj1 P) . 2) = - ((normalize_proj1 P) `2)
.= - ((u . 2) / (u . 1)) by A3 ;
A9: - ((normalize_proj1 P) . 3) = - ((normalize_proj1 P) `3)
.= - ((u . 3) / (u . 1)) by A3 ;
0 = |{(dir1a P),(dir1b P),u9}| by A5, A6, A7, BKMODEL1:1
.= |{|[(- ((normalize_proj1 P) . 2)),1,0]|,|[(- ((normalize_proj1 P) . 3)),0,1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
.= ((u9 `1) - ((- ((normalize_proj1 P) . 2)) * (u9 `2))) - ((- ((normalize_proj1 P) . 3)) * (u9 `3)) by Th2
.= ((u9 `1) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3)) by A8, A9 ;
then A10: 0 = (u . 1) * (((u9 `1) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3)))
.= (((u . 1) * (u9 `1)) + (((u . 1) * ((u . 2) / (u . 1))) * (u9 `2))) + (((u . 1) * ((u . 3) / (u . 1))) * (u9 `3))
.= (((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + (((u . 1) * ((u . 3) / (u . 1))) * (u9 `3)) by A2, Th10, XCMPLX_1:87
.= (((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)) by A2, Th10, XCMPLX_1:87 ;
set c2 = - ((normalize_proj2 P) . 1);
set c3 = - ((normalize_proj2 P) . 3);
A11: - ((normalize_proj2 P) . 1) = - ((normalize_proj2 P) `1)
.= - ((u . 1) / (u . 2)) by A3 ;
A12: - ((normalize_proj2 P) . 3) = - ((normalize_proj2 P) `3)
.= - ((u . 3) / (u . 2)) by A3 ;
|{|[1,(- ((normalize_proj2 P) . 1)),0]|,|[0,(- ((normalize_proj2 P) . 3)),1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}| = (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) - (u9 `2) by A11, A12, Th3;
then |{(dir2a P),(dir2b P),u9}| = (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- 1) * (u9 `2))
.= (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:60, A2, Th13
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + (((u . 2) / (- (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= (1 / (- (u . 2))) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.= 0 by A10 ;
then Pdir2a P, Pdir2b P,P9 are_collinear by A6, A7, BKMODEL1:1;
hence x in Line ((Pdir2a P),(Pdir2b P)) by A4; :: thesis: verum

end;

hence Line ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir2a P),(Pdir2b P)) ; :: thesis: Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir1a P),(Pdir1b P))

now :: thesis: for x being object st x in Line ((Pdir2a P),(Pdir2b P)) holds
x in Line ((Pdir1a P),(Pdir1b P))

let x be object ; :: thesis: ( x in Line ((Pdir2a P),(Pdir2b P)) implies x in Line ((Pdir1a P),(Pdir1b P)) )
assume x in Line ((Pdir2a P),(Pdir2b P)) ; :: thesis: x in Line ((Pdir1a P),(Pdir1b P))
then consider P9 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A13: x = P9 and
A14: Pdir2a P, Pdir2b P,P9 are_collinear ;
consider u9 being Element of (TOP-REAL 3) such that
A15: not u9 is zero and
A16: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - ((normalize_proj1 P) . 2);
set a3 = - ((normalize_proj1 P) . 3);
set b1 = u9 `1 ;
set b2 = u9 `2 ;
set b3 = u9 `3 ;
set c2 = - ((normalize_proj2 P) . 1);
set c3 = - ((normalize_proj2 P) . 3);
A17: - ((normalize_proj1 P) . 2) = - ((normalize_proj1 P) `2)
.= - ((u . 2) / (u . 1)) by A3 ;
A18: - ((normalize_proj1 P) . 3) = - ((normalize_proj1 P) `3)
.= - ((u . 3) / (u . 1)) by A3 ;
A19: - ((normalize_proj2 P) . 1) = - ((normalize_proj2 P) `1)
.= - ((u . 1) / (u . 2)) by A3 ;
A20: - ((normalize_proj2 P) . 3) = - ((normalize_proj2 P) `3)
.= - ((u . 3) / (u . 2)) by A3 ;
A21: - (u . 2) <> 0 by A2, Th13;
A22: 0 = |{(dir2a P),(dir2b P),u9}| by A14, A15, A16, BKMODEL1:1
.= |{|[1,(- ((normalize_proj2 P) . 1)),0]|,|[0,(- ((normalize_proj2 P) . 3)),1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
.= (((- ((normalize_proj2 P) . 3)) * (u9 `3)) + ((- ((normalize_proj2 P) . 1)) * (u9 `1))) - (u9 `2) by Th3
.= (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- 1) * (u9 `2)) by A19, A20
.= (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:60, A2, Th13
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= ((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + (((u . 2) / (- (u . 2))) * (u9 `2)) by XCMPLX_1:188
.= (1 / (- (u . 2))) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3))) ;
A23: (u . 1) / (u . 1) = 1 by XCMPLX_1:60, A2, Th10;
|{(dir1a P),(dir1b P),u9}| = |{|[(- ((normalize_proj1 P) . 2)),1,0]|,|[(- ((normalize_proj1 P) . 3)),0,1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
.= ((u9 `1) - ((- ((normalize_proj1 P) . 2)) * (u9 `2))) - ((- ((normalize_proj1 P) . 3)) * (u9 `3)) by Th2
.= ((((u . 1) / (u . 1)) * (u9 `1)) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3)) by A17, A18, A23
.= (1 / (u . 1)) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.= (1 / (u . 1)) * 0 by A22, A21, XCMPLX_1:6
.= 0 ;
then Pdir1a P, Pdir1b P,P9 are_collinear by A15, A16, BKMODEL1:1;
hence x in Line ((Pdir1a P),(Pdir1b P)) by A13; :: thesis: verum

end;

hence Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir1a P),(Pdir1b P)) ; :: thesis: verum

end;

hence dual1 P = dual2 P ; :: thesis: verum