let l, l1, m, m1 be Element of ProjectiveLines real_projective_plane; ex n being Element of ProjectiveLines real_projective_plane st
( l,l1,n are_concurrent & m,m1,n are_concurrent )
consider R being Point of real_projective_plane such that
A1:
dual l, dual l1,R are_collinear
and
A2:
dual m, dual m1,R are_collinear
by ANPROJ_2:def 14;
( dual (dual l), dual (dual l1), dual R are_concurrent & dual (dual m), dual (dual m1), dual R are_concurrent )
by A1, A2, Th59;
then
( l, dual (dual l1), dual R are_concurrent & m, dual (dual m1), dual R are_concurrent )
by Th46;
then
( l,l1, dual R are_concurrent & m,m1, dual R are_concurrent )
by Th46;
hence
ex n being Element of ProjectiveLines real_projective_plane st
( l,l1,n are_concurrent & m,m1,n are_concurrent )
; verum