let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for A, B, C being LINE of st ( A = B or B = C or C = A ) holds
A,B,C are_concurrent
let A, B, C be LINE of ; :: thesis: ( ( A = B or B = C or C = A ) implies A,B,C are_concurrent )
A1: ( ex a being POINT of st
( a on B & a on C ) & ex b being POINT of st
( b on C & b on A ) ) by INCPROJ:def 14;
assume ( A = B or B = C or C = A ) ; :: thesis: A,B,C are_concurrent
hence A,B,C are_concurrent by A1, Def1; :: thesis: verum