let IPP be IncProjSp; :: thesis: for a, b, c being POINT of
for A being LINE of 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 ; :: thesis: for A being LINE of 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 ; :: 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:12;
( a on A & b on A ) by A1, INCSP_1:12;
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:12; :: thesis: verum