let G be IncProjStr ; :: thesis: for a, b, c being POINT of G
for P, Q, R being LINE of G holds
( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) )
let a, b, c be POINT of G; :: thesis: for P, Q, R being LINE of G holds
( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) )
let P, Q, R be LINE of G; :: thesis: ( ( {a,b} on P implies {b,a} on P ) & ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) )
thus ( {a,b} on P implies {b,a} on P ) ; :: thesis: ( ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) & ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) )
thus ( {a,b,c} on P implies ( {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P ) ) :: thesis: ( ( a on P,Q implies a on Q,P ) & ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) ) ) thus ( a on P,Q implies a on Q,P ) ; :: thesis: ( a on P,Q,R implies ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) )
assume A3: a on P,Q,R ; :: thesis: ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P )
then A4: a on R ;
( a on P & a on Q ) by A3;
hence ( a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P ) by A4; :: thesis: verum