let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for A, B, C being LINE of IPP st A,B,C are_concurrent holds
( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent )
let A, B, C be LINE of IPP; :: thesis: ( A,B,C are_concurrent implies ( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent ) )
assume A,B,C are_concurrent ; :: thesis: ( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent )
then ex o being POINT of IPP st
( o on A & o on B & o on C ) by Def1;
hence ( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent ) by Def1; :: thesis: verum