let P be Point of real_projective_plane; :: thesis: for l being Element of ProjectiveLines real_projective_plane st P in l holds
dual l in dual P
let l be Element of ProjectiveLines real_projective_plane; :: thesis: ( P in l implies dual l in dual P )
assume A1: P in l ; :: thesis: dual l in dual P
consider u being Element of (TOP-REAL 3) such that
A2: not u is zero and
A3: P = Dir u by ANPROJ_1:26;
reconsider u = u as non zero Element of (TOP-REAL 3) by A2;
reconsider P9 = P as Element of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider dl = dual l as Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider Pl, Ql being Point of real_projective_plane such that
A4: Pl <> Ql and
A5: l = Line (Pl,Ql) and
A6: dual l = L2P (Pl,Ql) by Def25;
consider ul, vl being non zero Element of (TOP-REAL 3) such that
A7: Pl = Dir ul and
A8: Ql = Dir vl and
A9: L2P (Pl,Ql) = Dir (ul <X> vl) by A4, BKMODEL1:def 5;
reconsider ulvl = ul <X> vl as non zero Element of (TOP-REAL 3) by A4, A7, A8, BKMODEL1:78;
consider S being Point of real_projective_plane such that
A10: P = S and
A11: Pl,Ql,S are_collinear by A1, A5;
P,Pl,Ql are_collinear by A10, A11, ANPROJ_2:24;
then A12: |{u,ul,vl}| = 0 by A3, A7, A8, BKMODEL1:1;

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 l in dual P

then reconsider P9 = P9 as non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A13: P9 = P99 and
A14: dual P = dual1 P99 by Th38;
consider S being Point of real_projective_plane such that
A15: P = S and
A16: Pl,Ql,S are_collinear by A1, A5;
P,Pl,Ql are_collinear by A15, A16, ANPROJ_2:24;
then A17: |{u,ul,vl}| = 0 by A3, A7, A8, BKMODEL1:1;
Dir (normalize_proj1 P9) = Dir u by A3, Def2;
then A18: are_Prop normalize_proj1 P9,u by ANPROJ_1:22;
|{(dir1a P9),(dir1b P9),ulvl}| = |((normalize_proj1 P9),ulvl)| by Th21
.= 0 by A17, A18, Th7 ;
then Pdir1a P9, Pdir1b P9,dl are_collinear by A6, A9, BKMODEL1:1;
hence dual l in dual P by A13, A14; :: thesis: verum

end;

suppose not P9 is zero_proj2 ; :: thesis: dual l in dual P

then reconsider P9 = P9 as non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A19: P9 = P99 and
A20: dual P = dual2 P99 by Th39;
Dir (normalize_proj2 P9) = Dir u by A3, Def4;
then A21: are_Prop normalize_proj2 P9,u by ANPROJ_1:22;
|{(dir2a P9),(dir2b P9),ulvl}| = - |((normalize_proj2 P9),ulvl)| by Th25
.= - 0 by A12, A21, Th7 ;
then Pdir2a P9, Pdir2b P9,dl are_collinear by A6, A9, BKMODEL1:1;
hence dual l in dual P by A19, A20; :: thesis: verum

end;

suppose not P9 is zero_proj3 ; :: thesis: dual l in dual P

then reconsider P9 = P9 as non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A22: P9 = P99 and
A23: dual P = dual3 P99 by Th40;
Dir (normalize_proj3 P9) = Dir u by A3, Def6;
then A24: are_Prop normalize_proj3 P9,u by ANPROJ_1:22;
|{(dir3a P9),(dir3b P9),ulvl}| = |((normalize_proj3 P9),ulvl)| by Th29
.= 0 by A12, A24, Th7 ;
then Pdir3a P9, Pdir3b P9,dl are_collinear by A6, A9, BKMODEL1:1;
hence dual l in dual P by A22, A23; :: thesis: verum

end;

end;