theorem
for
l1,
n2,
m,
n1,
m1,
l,
n being
Element of
ProjectiveLines real_projective_plane st
l1,
n2,
m are_concurrent &
n1,
m1,
m are_concurrent &
l1,
n1,
l are_concurrent &
n2,
m1,
l are_concurrent &
l1,
m1,
n are_concurrent &
n2,
n1,
n are_concurrent &
l,
m,
n are_concurrent & not
l1,
n2,
m1 are_concurrent & not
l1,
n2,
n1 are_concurrent & not
l1,
n1,
m1 are_concurrent holds
n2,
n1,
m1 are_concurrent