let l, m be 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 )
consider r being Point of real_projective_plane such that
A1:
dual l <> r
and
A2:
dual m <> r
and
A3:
dual l, dual m,r are_collinear
by ANPROJ_2:def 10;
now ( l <> dual r & m <> dual r & l,m, dual r are_concurrent )thus
(
l <> dual r &
m <> dual r )
by Th45, A1, A2;
l,m, dual r are_concurrent
dual (dual l),
dual (dual m),
dual r are_concurrent
by A3, Th59;
then
l,
dual (dual m),
dual r are_concurrent
by Th46;
hence
l,
m,
dual r are_concurrent
by Th46;
verum end;
hence
ex n being Element of ProjectiveLines real_projective_plane st
( l <> n & m <> n & l,m,n are_concurrent )
; verum