let P be Point of real_projective_plane; :: thesis: dual (dual P) = P
reconsider P9 = P as Point of (ProjectiveSpace (TOP-REAL 3)) ;

per cases ( not P9 is zero_proj1 or not P9 is zero_proj2 or not P9 is zero_proj3 ) by Th37;

suppose not P9 is zero_proj1 ; :: thesis: dual (dual P) = P

then reconsider P9 = P as non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider P = P9 as Point of real_projective_plane ;
consider P99 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A1: ( P = P99 & dual P = dual1 P99 ) by Th38;
reconsider l = Line ((Pdir1a P9),(Pdir1b P9)) as Element of ProjectiveLines real_projective_plane by A1;
consider P1, P2 being Point of real_projective_plane such that
A2: P1 <> P2 and
A3: l = Line (P1,P2) and
A4: dual l = L2P (P1,P2) by Def25;
A5: ( Line (P1,P2) = Line ((Pdir1a P9),(Pdir1b P9)) & P1 in Line (P1,P2) & P2 in Line (P1,P2) ) by A3, COLLSP:10;
then consider Q1 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A6: P1 = Q1 and
A7: Pdir1a P9, Pdir1b P9,Q1 are_collinear ;
consider Q2 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A8: P2 = Q2 and
A9: Pdir1a P9, Pdir1b P9,Q2 are_collinear by A5;
consider u, v being non zero Element of (TOP-REAL 3) such that
A10: P1 = Dir u and
A11: P2 = Dir v and
A12: L2P (P1,P2) = Dir (u <X> v) by A2, BKMODEL1:def 5;
consider w being Element of (TOP-REAL 3) such that
A13: not w is zero and
A14: P9 = Dir w by ANPROJ_1:26;
reconsider w = w as non zero Element of (TOP-REAL 3) by A13;
normalize_proj1 P9 = |[1,((w . 2) / (w . 1)),((w . 3) / (w . 1))]| by A14, Th11;
then ( (normalize_proj1 P9) `2 = (w . 2) / (w . 1) & (normalize_proj1 P9) `3 = (w . 3) / (w . 1) ) ;
then A15: (dir1a P9) <X> (dir1b P9) = |[((1 * 1) - (0 * 0)),((0 * (- ((w . 3) / (w . 1)))) - ((- ((w . 2) / (w . 1))) * 1)),(((- ((w . 2) / (w . 1))) * 0) - ((- ((w . 3) / (w . 1))) * 1))]|
.= |[((w `1) / (w . 1)),((w `2) / (w . 1)),((w `3) / (w . 1))]| by A14, Th10, XCMPLX_1:60
.= (1 / (w . 1)) * w by EUCLID_5:7 ;
w . 1 <> 0 by A14, Th10;
then reconsider a = (1 / (w . 1)) * w as non zero Element of (TOP-REAL 3) by ANPROJ_9:3;

now :: thesis: not u <X> v = 0. (TOP-REAL 3)

assume u <X> v = 0. (TOP-REAL 3) ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A2, A10, A11, ANPROJ_1:22; :: thesis: verum

end;

then A16: not u <X> v is zero ;

now :: thesis: ( are_Prop (w . 1) * a,u <X> v & (w . 1) * a = w )

now :: thesis: ( not are_Prop u,v & 0 = |(a,u)| & 0 = |(a,v)| )

thus not are_Prop u,v by A2, A10, A11, ANPROJ_1:22; :: thesis: ( 0 = |(a,u)| & 0 = |(a,v)| )
thus 0 = |{(dir1a P9),(dir1b P9),u}| by A10, A6, A7, BKMODEL1:1
.= |{u,(dir1a P9),(dir1b P9)}| by EUCLID_5:34
.= |(a,u)| by A15 ; :: thesis: 0 = |(a,v)|
thus 0 = |{(dir1a P9),(dir1b P9),v}| by A11, A8, A9, BKMODEL1:1
.= |{v,(dir1a P9),(dir1b P9)}| by EUCLID_5:34
.= |(a,v)| by A15 ; :: thesis: verum

end;

then are_Prop (1 / (w . 1)) * w,u <X> v by Th8;
hence are_Prop (w . 1) * a,u <X> v by A14, Th10, A16, Th9; :: thesis: (w . 1) * a = w
thus (w . 1) * a = ((w . 1) * (1 / (w . 1))) * w by RVSUM_1:49
.= 1 * w by A14, Th10, XCMPLX_1:106
.= w by RVSUM_1:52 ; :: thesis: verum

end;

hence dual (dual P) = P by A14, A1, A4, A12, A16, ANPROJ_1:22; :: thesis: verum

end;

suppose not P9 is zero_proj2 ; :: thesis: dual (dual P) = P

then reconsider P9 = P as non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider P = P9 as Point of real_projective_plane ;
consider P99 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A17: ( P = P99 & dual P = dual2 P99 ) by Th39;
reconsider l = Line ((Pdir2a P9),(Pdir2b P9)) as Element of ProjectiveLines real_projective_plane by A17;
consider P1, P2 being Point of real_projective_plane such that
A18: P1 <> P2 and
A19: l = Line (P1,P2) and
A20: dual l = L2P (P1,P2) by Def25;
A21: ( Line (P1,P2) = Line ((Pdir2a P9),(Pdir2b P9)) & P1 in Line (P1,P2) & P2 in Line (P1,P2) ) by A19, COLLSP:10;
then consider Q1 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A22: P1 = Q1 and
A23: Pdir2a P9, Pdir2b P9,Q1 are_collinear ;
consider Q2 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A24: P2 = Q2 and
A25: Pdir2a P9, Pdir2b P9,Q2 are_collinear by A21;
consider u, v being non zero Element of (TOP-REAL 3) such that
A26: P1 = Dir u and
A27: P2 = Dir v and
A28: L2P (P1,P2) = Dir (u <X> v) by A18, BKMODEL1:def 5;
consider w being Element of (TOP-REAL 3) such that
A29: not w is zero and
A30: P9 = Dir w by ANPROJ_1:26;
reconsider w = w as non zero Element of (TOP-REAL 3) by A29;
normalize_proj2 P9 = |[((w . 1) / (w . 2)),1,((w . 3) / (w . 2))]| by A30, Th14;
then ( (normalize_proj2 P9) `1 = (w . 1) / (w . 2) & (normalize_proj2 P9) `3 = (w . 3) / (w . 2) ) ;
then A31: (dir2a P9) <X> (dir2b P9) = |[(((- ((w . 1) / (w . 2))) * 1) - (0 * (- ((w . 3) / (w . 2))))),((0 * 0) - (1 * 1)),((1 * (- ((w . 3) / (w . 2)))) - (0 * (- ((w . 1) / (w . 2)))))]|
.= |[(- ((w . 1) / (w . 2))),(- ((w . 2) / (w . 2))),(- ((w . 3) / (w . 2)))]| by A30, Th13, XCMPLX_1:60
.= |[((w . 1) / (- (w . 2))),(- ((w . 2) / (w . 2))),(- ((w . 3) / (w . 2)))]| by XCMPLX_1:188
.= |[((w . 1) / (- (w . 2))),((w . 2) / (- (w . 2))),(- ((w . 3) / (w . 2)))]| by XCMPLX_1:188
.= |[((w `1) / (- (w . 2))),((w `2) / (- (w . 2))),((w `3) / (- (w . 2)))]| by XCMPLX_1:188
.= (1 / (- (w . 2))) * w by EUCLID_5:7 ;
A32: w . 2 <> 0 by A30, Th13;
then reconsider a = (1 / (- (w . 2))) * w as non zero Element of (TOP-REAL 3) by ANPROJ_9:3;

now :: thesis: not u <X> v = 0. (TOP-REAL 3)

assume u <X> v = 0. (TOP-REAL 3) ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A18, A26, A27, ANPROJ_1:22; :: thesis: verum

end;

then A33: not u <X> v is zero ;

now :: thesis: ( are_Prop (- (w . 2)) * a,u <X> v & (- (w . 2)) * a = w )

now :: thesis: ( not are_Prop u,v & 0 = |(a,u)| & 0 = |(a,v)| )

thus not are_Prop u,v by A18, A26, A27, ANPROJ_1:22; :: thesis: ( 0 = |(a,u)| & 0 = |(a,v)| )
thus 0 = |{(dir2a P9),(dir2b P9),u}| by A26, A22, A23, BKMODEL1:1
.= |{u,(dir2a P9),(dir2b P9)}| by EUCLID_5:34
.= |(a,u)| by A31 ; :: thesis: 0 = |(a,v)|
thus 0 = |{(dir2a P9),(dir2b P9),v}| by A27, A24, A25, BKMODEL1:1
.= |{v,(dir2a P9),(dir2b P9)}| by EUCLID_5:34
.= |(a,v)| by A31 ; :: thesis: verum

end;

then are_Prop (1 / (- (w . 2))) * w,u <X> v by Th8;
hence are_Prop (- (w . 2)) * a,u <X> v by A32, A33, Th9; :: thesis: (- (w . 2)) * a = w
thus (- (w . 2)) * a = ((- (w . 2)) * (1 / (- (w . 2)))) * w by RVSUM_1:49
.= 1 * w by A32, XCMPLX_1:106
.= w by RVSUM_1:52 ; :: thesis: verum

end;

hence dual (dual P) = P by A30, A17, A20, A28, A33, ANPROJ_1:22; :: thesis: verum

end;

suppose not P9 is zero_proj3 ; :: thesis: dual (dual P) = P

then reconsider P9 = P as non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider P = P9 as Point of real_projective_plane ;
consider P99 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A34: ( P = P99 & dual P = dual3 P99 ) by Th40;
reconsider l = Line ((Pdir3a P9),(Pdir3b P9)) as Element of ProjectiveLines real_projective_plane by A34;
consider P1, P2 being Point of real_projective_plane such that
A35: P1 <> P2 and
A36: l = Line (P1,P2) and
A37: dual l = L2P (P1,P2) by Def25;
A38: ( Line (P1,P2) = Line ((Pdir3a P9),(Pdir3b P9)) & P1 in Line (P1,P2) & P2 in Line (P1,P2) ) by A36, COLLSP:10;
then consider Q1 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A39: P1 = Q1 and
A40: Pdir3a P9, Pdir3b P9,Q1 are_collinear ;
consider Q2 being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A41: P2 = Q2 and
A42: Pdir3a P9, Pdir3b P9,Q2 are_collinear by A38;
consider u, v being non zero Element of (TOP-REAL 3) such that
A43: P1 = Dir u and
A44: P2 = Dir v and
A45: L2P (P1,P2) = Dir (u <X> v) by A35, BKMODEL1:def 5;
consider w being Element of (TOP-REAL 3) such that
A46: not w is zero and
A47: P9 = Dir w by ANPROJ_1:26;
reconsider w = w as non zero Element of (TOP-REAL 3) by A46;
normalize_proj3 P9 = |[((w . 1) / (w . 3)),((w . 2) / (w . 3)),1]| by A47, Th17;
then ( (normalize_proj3 P9) `1 = (w . 1) / (w . 3) & (normalize_proj3 P9) `2 = (w . 2) / (w . 3) ) ;
then A48: (dir3a P9) <X> (dir3b P9) = |[((0 * (- ((w . 2) / (w . 3)))) - ((- ((w . 1) / (w . 3))) * 1)),(((- ((w . 1) / (w . 3))) * 0) - (1 * (- ((w . 2) / (w . 3))))),((1 * 1) - (0 * 0))]|
.= |[((w `1) / (w . 3)),((w `2) / (w . 3)),((w `3) / (w . 3))]| by A47, Th16, XCMPLX_1:60
.= (1 / (w . 3)) * w by EUCLID_5:7 ;
w . 3 <> 0 by A47, Th16;
then reconsider a = (1 / (w . 3)) * w as non zero Element of (TOP-REAL 3) by ANPROJ_9:3;

now :: thesis: not u <X> v = 0. (TOP-REAL 3)

assume u <X> v = 0. (TOP-REAL 3) ; :: thesis: contradiction
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A35, A43, A44, ANPROJ_1:22; :: thesis: verum

end;

then A49: not u <X> v is zero ;

now :: thesis: ( are_Prop (w . 3) * a,u <X> v & (w . 3) * a = w )

now :: thesis: ( not are_Prop u,v & 0 = |(a,u)| & 0 = |(a,v)| )

thus not are_Prop u,v by A35, A43, A44, ANPROJ_1:22; :: thesis: ( 0 = |(a,u)| & 0 = |(a,v)| )
thus 0 = |{(dir3a P9),(dir3b P9),u}| by A43, A39, A40, BKMODEL1:1
.= |{u,(dir3a P9),(dir3b P9)}| by EUCLID_5:34
.= |(a,u)| by A48 ; :: thesis: 0 = |(a,v)|
thus 0 = |{(dir3a P9),(dir3b P9),v}| by A44, A41, A42, BKMODEL1:1
.= |{v,(dir3a P9),(dir3b P9)}| by EUCLID_5:34
.= |(a,v)| by A48 ; :: thesis: verum

end;

then are_Prop (1 / (w . 3)) * w,u <X> v by Th8;
hence are_Prop (w . 3) * a,u <X> v by A47, Th16, A49, Th9; :: thesis: (w . 3) * a = w
thus (w . 3) * a = ((w . 3) * (1 / (w . 3))) * w by RVSUM_1:49
.= 1 * w by A47, Th16, XCMPLX_1:106
.= w by RVSUM_1:52 ; :: thesis: verum

end;

hence dual (dual P) = P by A47, A34, A37, A45, A49, ANPROJ_1:22; :: thesis: verum

end;

end;