let l1, l2, l3 be Element of ProjectiveLines real_projective_plane; :: thesis: ( l1,l2,l3 are_concurrent implies dual l1, dual l2, dual l3 are_collinear )
assume l1,l2,l3 are_concurrent ; :: thesis: 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; :: thesis: verum