let IPP be IncProjSp; 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; 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; ( {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
; ( {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; verum