theorem :: ANPROJ11:65

for l, m being Element of ProjectiveLines real_projective_plane ex n being Element of ProjectiveLines real_projective_plane st
( l <> n & m <> n & l,m,n are_concurrent )