let P, Q, R be Point of real_projective_plane; :: thesis: ( P,Q,R are_collinear implies dual P, dual Q, dual R are_concurrent )
assume A1: P,Q,R are_collinear ; :: thesis: dual P, dual Q, dual R are_concurrent
per cases ( Q = R or Q <> R ) ;
suppose A2: Q = R ; :: thesis: dual P, dual Q, dual R are_concurrent
reconsider lP = dual P, lQ = dual Q as LINE of real_projective_plane by INCPROJ:1;
ex x being object st
( x in lP & x in lQ ) by BKMODEL1:76, XBOOLE_0:3;
hence dual P, dual Q, dual R are_concurrent by A2; :: thesis: verum
end;
suppose A3: Q <> R ; :: thesis: dual P, dual Q, dual R are_concurrent
A4: Q,R,P are_collinear by A1, ANPROJ_2:24;
reconsider l = Line (Q,R) as LINE of real_projective_plane by A3, COLLSP:def 7;
l in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } ;
then reconsider l = Line (Q,R) as Element of ProjectiveLines real_projective_plane ;
( dual l in dual P & dual l in dual Q & dual l in dual R ) by A4, COLLSP:11, Th54, COLLSP:10;
hence dual P, dual Q, dual R are_concurrent ; :: thesis: verum
end;
end;