let P be non zero_proj1 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: dual1 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_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| & normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| ) by A2, Th11, Th17;

now :: thesis: ( Line ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir3a P),(Pdir3b P)) & Line ((Pdir3a P),(Pdir3b 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 ((Pdir3a P),(Pdir3b P))

let x be object ; :: thesis: ( x in Line ((Pdir1a P),(Pdir1b P)) implies x in Line ((Pdir3a P),(Pdir3b P)) )
assume x in Line ((Pdir1a P),(Pdir1b 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: 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_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 ;
|{|[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;
then |{(dir3a P),(dir3b P),u9}| = ((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (1 * (u9 `3)) by A11, A12
.= ((((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)))
.= 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 ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir3a P),(Pdir3b P)) ; :: thesis: Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir1a P),(Pdir1b P))

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

let x be object ; :: thesis: ( x in Line ((Pdir3a P),(Pdir3b P)) implies x in Line ((Pdir1a P),(Pdir1b P)) )
assume x in Line ((Pdir3a P),(Pdir3b 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: Pdir3a P, Pdir3b 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_proj3 P) . 1);
set c3 = - ((normalize_proj3 P) . 2);
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_proj3 P) . 1) = - ((normalize_proj3 P) `1)
.= - ((u . 1) / (u . 3)) by A3 ;
A20: - ((normalize_proj3 P) . 2) = - ((normalize_proj3 P) `2)
.= - ((u . 2) / (u . 3)) by A3 ;
A21: 0 = |{(dir3a P),(dir3b P),u9}| by A14, A15, A16, 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 A19, A20
.= ((((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))) ;
A22: u . 3 <> 0 by A2, Th16;
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 ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir1a P),(Pdir1b P)) ; :: thesis: verum

end;

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