let P be non zero_proj2 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: dual2 P = dual3 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_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| & normalize_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]| ) by A2, Th17, Th14;

now :: thesis: ( Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir3a P),(Pdir3b P)) & Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir2a P),(Pdir2b P)) )

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

let x be object ; :: thesis: ( x in Line ((Pdir2a P),(Pdir2b P)) implies x in Line ((Pdir3a P),(Pdir3b P)) )
assume x in Line ((Pdir2a P),(Pdir2b P)) ; :: thesis: x in Line ((Pdir3a P),(Pdir3b P))
then consider P9 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A4: x = P9 and
A5: Pdir2a P, Pdir2b 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_proj2 P) . 1);
set a3 = - ((normalize_proj2 P) . 3);
set b1 = u9 `1 ;
set b2 = u9 `2 ;
set b3 = u9 `3 ;
A8: - ((normalize_proj2 P) . 1) = - ((normalize_proj2 P) `1)
.= - ((u . 1) / (u . 2)) by A3 ;
A9: - ((normalize_proj2 P) . 3) = - ((normalize_proj2 P) `3)
.= - ((u . 3) / (u . 2)) by A3 ;
0 = |{(dir2a P),(dir2b P),u9}| by A5, A6, A7, BKMODEL1:1
.= |{|[1,(- ((normalize_proj2 P) . 1)),0]|,|[0,(- ((normalize_proj2 P) . 3)),1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
.= (((- ((normalize_proj2 P) . 1)) * (u9 `1)) + ((- ((normalize_proj2 P) . 3)) * (u9 `3))) - (u9 `2) by Th3
.= - (((((u . 1) / (u . 2)) * (u9 `1)) + (u9 `2)) + (((u . 3) / (u . 2)) * (u9 `3))) by A8, A9 ;
then A10: 0 = (u . 2) * (((((u . 1) / (u . 2)) * (u9 `1)) + (u9 `2)) + (((u . 3) / (u . 2)) * (u9 `3)))
.= (((u . 2) * (u9 `2)) + (((u . 2) * ((u . 1) / (u . 2))) * (u9 `1))) + (((u . 2) * ((u . 3) / (u . 2))) * (u9 `3))
.= (((u . 2) * (u9 `2)) + ((u . 1) * (u9 `1))) + (((u . 2) * ((u . 3) / (u . 2))) * (u9 `3)) by A2, Th13, XCMPLX_1:87
.= (((u . 2) * (u9 `2)) + ((u . 1) * (u9 `1))) + ((u . 3) * (u9 `3)) by A2, Th13, XCMPLX_1:87 ;
set c2 = - ((normalize_proj3 P) . 1);
set c3 = - ((normalize_proj3 P) . 2);
A11: - ((normalize_proj3 P) . 1) = - ((normalize_proj3 P) `1)
.= - ((u . 1) / (u . 3)) by A3 ;
A12: - ((normalize_proj3 P) . 2) = - ((normalize_proj3 P) `2)
.= - ((u . 2) / (u . 3)) by A3 ;
A13: (u . 3) / (u . 3) = 1 by A2, Th16, XCMPLX_1:60;
|{|[1,0,(- ((normalize_proj3 P) . 1))]|,|[0,1,(- ((normalize_proj3 P) . 2))]|,|[(u9 `1),(u9 `2),(u9 `3)]|}| = ((u9 `3) - ((u9 `1) * (- ((u . 1) / (u . 3))))) - ((u9 `2) * (- ((u . 2) / (u . 3)))) by A11, A12, Th4
.= ((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (u9 `3) ;
then |{(dir3a P),(dir3b P),u9}| = ((((u . 1) * (1 / (u . 3))) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (((u . 3) / (u . 3)) * (u9 `3)) by A13
.= (1 / (u . 3)) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.= 0 by A10 ;
then Pdir3a P, Pdir3b P,P9 are_collinear by A6, A7, BKMODEL1:1;
hence x in Line ((Pdir3a P),(Pdir3b P)) by A4; :: thesis: verum

end;

hence Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir3a P),(Pdir3b P)) ; :: thesis: Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir2a P),(Pdir2b P))

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

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

end;

hence Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir2a P),(Pdir2b P)) ; :: thesis: verum

end;

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