let G be IncProjStr ; for a, p, q, r being POINT of G
for P, Q, R, A being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R holds
p,q,r are_mutually_different
let a, p, q, r be POINT of G; for P, Q, R, A being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R holds
p,q,r are_mutually_different
let P, Q, R, A be LINE of G; ( G is configuration & a on P,Q,R & P,Q,R are_mutually_different & a |' A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_different )
assume that
A1:
G is configuration
and
A2:
a on P,Q,R
and
A3:
P,Q,R are_mutually_different
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_different
A8:
( a on R & r on R )
by A2, A7, Def2, Def3;
A9:
( a on Q & q on Q )
by A2, A6, Def2, Def3;
( Q <> R & q on A )
by A3, A6, Def2, ZFMISC_1:def 5;
then A10:
q <> r
by A1, A4, A9, A8, Def4;
A11:
p on P
by A5, Def2;
A12:
( a on P & p on A )
by A2, A5, Def2, Def3;
R <> P
by A3, ZFMISC_1:def 5;
then A13:
r <> p
by A1, A4, A12, A11, A8, Def4;
P <> Q
by A3, ZFMISC_1:def 5;
then
p <> q
by A1, A4, A12, A11, A9, Def4;
hence
p,q,r are_mutually_different
by A10, A13, ZFMISC_1:def 5; verum