let G be IncProjStr ; :: thesis: for a, p, q, r being POINT of G

for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds

p,q,r are_mutually_distinct

let a, p, q, r be POINT of G; :: thesis: for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds

p,q,r are_mutually_distinct

let A, P, Q, R be LINE of G; :: thesis: ( G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_distinct )

assume that

A1: G is configuration and

A2: a on P,Q,R and

A3: P,Q,R are_mutually_distinct and

A4: a |' A and

A5: p on A,P and

A6: q on A,Q and

A7: r on A,R ; :: thesis: p,q,r are_mutually_distinct

A8: ( a on R & r on R ) by A2, A7;

A9: ( a on Q & q on Q ) by A2, A6;

( Q <> R & q on A ) by A3, A6, ZFMISC_1:def 5;

then A10: q <> r by A1, A4, A9, A8;

A11: p on P by A5;

A12: ( a on P & p on A ) by A2, A5;

R <> P by A3, ZFMISC_1:def 5;

then A13: r <> p by A1, A4, A12, A11, A8;

P <> Q by A3, ZFMISC_1:def 5;

then p <> q by A1, A4, A12, A11, A9;

hence p,q,r are_mutually_distinct by A10, A13, ZFMISC_1:def 5; :: thesis: verum

for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds

p,q,r are_mutually_distinct

let a, p, q, r be POINT of G; :: thesis: for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds

p,q,r are_mutually_distinct

let A, P, Q, R be LINE of G; :: thesis: ( G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_distinct )

assume that

A1: G is configuration and

A2: a on P,Q,R and

A3: P,Q,R are_mutually_distinct and

A4: a |' A and

A5: p on A,P and

A6: q on A,Q and

A7: r on A,R ; :: thesis: p,q,r are_mutually_distinct

A8: ( a on R & r on R ) by A2, A7;

A9: ( a on Q & q on Q ) by A2, A6;

( Q <> R & q on A ) by A3, A6, ZFMISC_1:def 5;

then A10: q <> r by A1, A4, A9, A8;

A11: p on P by A5;

A12: ( a on P & p on A ) by A2, A5;

R <> P by A3, ZFMISC_1:def 5;

then A13: r <> p by A1, A4, A12, A11, A8;

P <> Q by A3, ZFMISC_1:def 5;

then p <> q by A1, A4, A12, A11, A9;

hence p,q,r are_mutually_distinct by A10, A13, ZFMISC_1:def 5; :: thesis: verum