let G be IncProjStr ; 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; 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; ( 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
; 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; verum