let l, l1, l2, n, n1 be Element of ProjectiveLines real_projective_plane; :: thesis: ( l,l1,n are_concurrent & l1,l2,n1 are_concurrent implies ex n2 being Element of ProjectiveLines real_projective_plane st
( l,l2,n2 are_concurrent & n,n1,n2 are_concurrent ) )
assume that
A1: l,l1,n are_concurrent and
A2: l1,l2,n1 are_concurrent ; :: thesis: ex n2 being Element of ProjectiveLines real_projective_plane st
( l,l2,n2 are_concurrent & n,n1,n2 are_concurrent )
( dual l, dual l1, dual n are_collinear & dual l1, dual l2, dual n1 are_collinear ) by A1, A2, Th60;
then consider P being Point of real_projective_plane such that
A3: dual l, dual l2,P are_collinear and
A4: dual n, dual n1,P are_collinear by ANPROJ_2:def 9;
take dual P ; :: thesis: ( l,l2, dual P are_concurrent & n,n1, dual P are_concurrent )
( dual (dual l), dual (dual l2), dual P are_concurrent & dual (dual n), dual (dual n1), dual P are_concurrent ) by A3, A4, Th59;
then ( l, dual (dual l2), dual P are_concurrent & n, dual (dual n1), dual P are_concurrent ) by Th46;
hence ( l,l2, dual P are_concurrent & n,n1, dual P are_concurrent ) by Th46; :: thesis: verum