let l1, l2, l3 be Element of ProjectiveLines real_projective_plane; :: thesis: ( l1,l2,l1 are_concurrent & l1,l1,l2 are_concurrent & l1,l2,l2 are_concurrent )
( dual l1, dual l2, dual l1 are_collinear & dual l1, dual l1, dual l2 are_collinear & dual l1, dual l2, dual l2 are_collinear ) by ANPROJ_2:def 7;
then ( dual (dual l1), dual (dual l2), dual (dual l1) are_concurrent & dual (dual l1), dual (dual l1), dual (dual l2) are_concurrent & dual (dual l1), dual (dual l2), dual (dual l2) are_concurrent ) by Th59;
then ( l1, dual (dual l2), dual (dual l1) are_concurrent & l1, dual (dual l1), dual (dual l2) are_concurrent & l1, dual (dual l2), dual (dual l2) are_concurrent ) by Th46;
then ( l1,l2, dual (dual l1) are_concurrent & l1,l1, dual (dual l2) are_concurrent & l1,l2, dual (dual l2) are_concurrent ) by Th46;
hence ( l1,l2,l1 are_concurrent & l1,l1,l2 are_concurrent & l1,l2,l2 are_concurrent ) ; :: thesis: verum