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