let l1, l2, l3 be Element of ProjectiveLines real_projective_plane; :: thesis:

now :: thesis:

l1 in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } ;
hence ex B being Subset of real_projective_plane st
( l1 = B & B is LINE of real_projective_plane ) ; :: thesis:
l2 in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } ;
hence ex B being Subset of real_projective_plane st
( l2 = B & B is LINE of real_projective_plane ) ; :: thesis:
l3 in { B where B is Subset of real_projective_plane : B is LINE of real_projective_plane } ;
hence ex B being Subset of real_projective_plane st
( l3 = B & B is LINE of real_projective_plane ) ; :: thesis:

end;

then reconsider m1 = l1, m2 = l2, m3 = l3 as LINE of real_projective_plane ;
reconsider l91 = # l1, l92 = # l2, l93 = # l3 as LINE of (IncProjSp_of real_projective_plane) ;

hereby :: thesis:

assume l1,l2,l3 are_concurrent ; :: thesis:
then consider P being Point of real_projective_plane such that
A1: P in l1 and
A2: P in l2 and
A3: P in l3 ;
reconsider P = P as Element of the Points of (IncProjSp_of real_projective_plane) ;
reconsider P9 = P as POINT of (IncProjSp_of real_projective_plane) ;
( P in m1 & P in m2 & P in m3 ) by A1, A2, A3;
then ( P9 on l91 & P9 on l92 & P9 on l93 ) by INCPROJ:5;
hence # l1, # l2, # l3 are_concurrent ; :: thesis:

end;

assume # l1, # l2, # l3 are_concurrent ; :: thesis:
then consider o being Element of the Points of (IncProjSp_of real_projective_plane) such that
A4: o on # l1 and
A5: o on # l2 and
A6: o on # l3 ;
reconsider o9 = o as Point of real_projective_plane ;
( o9 in m1 & o9 in m2 & o9 in m3 ) by A4, A5, A6, INCPROJ:5;
hence l1,l2,l3 are_concurrent ; :: thesis: