let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for A, B, C being LINE of IPP st ( A = B or B = C or C = A ) holds

A,B,C are_concurrent

let A, B, C be LINE of IPP; :: thesis: ( ( A = B or B = C or C = A ) implies A,B,C are_concurrent )

A1: ( ex a being POINT of IPP st

( a on B & a on C ) & ex b being POINT of IPP st

( b on C & b on A ) ) by INCPROJ:def 9;

assume ( A = B or B = C or C = A ) ; :: thesis: A,B,C are_concurrent

hence A,B,C are_concurrent by A1; :: thesis: verum

A,B,C are_concurrent

let A, B, C be LINE of IPP; :: thesis: ( ( A = B or B = C or C = A ) implies A,B,C are_concurrent )

A1: ( ex a being POINT of IPP st

( a on B & a on C ) & ex b being POINT of IPP st

( b on C & b on A ) ) by INCPROJ:def 9;

assume ( A = B or B = C or C = A ) ; :: thesis: A,B,C are_concurrent

hence A,B,C are_concurrent by A1; :: thesis: verum