let l1, l2, l3 be Element of ProjectiveLines real_projective_plane; ( l1,l2,l3 are_concurrent implies dual l1, dual l2, dual l3 are_collinear )
assume
l1,l2,l3 are_concurrent
; dual l1, dual l2, dual l3 are_collinear
then consider P being Point of real_projective_plane such that
A1:
( P in l1 & P in l2 & P in l3 )
;
reconsider lP = dual P as Element of ProjectiveLines real_projective_plane ;
( dual l1 in lP & dual l2 in lP & dual l3 in lP )
by A1, Th54;
hence
dual l1, dual l2, dual l3 are_collinear
by Th57; verum