let IPP be IncProjSp; :: thesis: for a, b, c being POINT of IPP
for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
let a, b, c be POINT of IPP; :: thesis: for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
let A be LINE of IPP; :: thesis: ( {a,b,c} on A implies ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) )
assume A1: {a,b,c} on A ; :: thesis: ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
then A2: c on A by INCSP_1:2;
( a on A & b on A ) by A1, INCSP_1:2;
hence ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) by A2, INCSP_1:2; :: thesis: verum