let l, m be Element of ProjectiveLines real_projective_plane; :: thesis: ex n being Element of ProjectiveLines real_projective_plane st
( l <> n & m <> n & l,m,n are_concurrent )
consider r being Point of real_projective_plane such that
A1: dual l <> r and
A2: dual m <> r and
A3: dual l, dual m,r are_collinear by ANPROJ_2:def 10;

now :: thesis: ( l <> dual r & m <> dual r & l,m, dual r are_concurrent )

thus ( l <> dual r & m <> dual r ) by Th45, A1, A2; :: thesis: l,m, dual r are_concurrent
dual (dual l), dual (dual m), dual r are_concurrent by A3, Th59;
then l, dual (dual m), dual r are_concurrent by Th46;
hence l,m, dual r are_concurrent by Th46; :: thesis: verum

end;

hence ex n being Element of ProjectiveLines real_projective_plane st
( l <> n & m <> n & l,m,n are_concurrent ) ; :: thesis: verum