let l, m, n, n1, n2 be Element of ProjectiveLines real_projective_plane; :: thesis: ( l <> m & l,m,n are_concurrent & l,m,n1 are_concurrent & l,m,n2 are_concurrent implies n,n1,n2 are_concurrent )
assume that
A1: l <> m and
A2: l,m,n are_concurrent and
A3: l,m,n1 are_concurrent and
A4: l,m,n2 are_concurrent ; :: thesis: n,n1,n2 are_concurrent
( dual l <> dual m & dual l, dual m, dual n are_collinear & dual l, dual m, dual n1 are_collinear & dual l, dual m, dual n2 are_collinear ) by A1, A2, A3, A4, Th60, Th48;
then dual (dual n), dual (dual n1), dual (dual n2) are_concurrent by ANPROJ_2:def 8, Th59;
then n, dual (dual n1), dual (dual n2) are_concurrent by Th46;
then n,n1, dual (dual n2) are_concurrent by Th46;
hence n,n1,n2 are_concurrent by Th46; :: thesis: verum