let AFP be AffinPlane; for a, b, p, q being Element of AFP st ( for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q ) & a,b // p,q & a,p // b,q & not LIN a,b,p holds
a,q // b,p
let a, b, p, q be Element of AFP; ( ( for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q ) & a,b // p,q & a,p // b,q & not LIN a,b,p implies a,q // b,p )
assume that
A1:
for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q
and
A2:
a,b // p,q
and
A3:
a,p // b,q
and
A4:
not LIN a,b,p
; a,q // b,p
consider z being Element of AFP such that
A5:
q,p // a,z
and
A6:
q,a // p,z
by DIRAF:40;
A7:
p <> q
A8:
not LIN a,p,q
proof
A9:
LIN p,
q,
p
by AFF_1:7;
assume
LIN a,
p,
q
;
contradiction
then A10:
LIN p,
q,
a
by AFF_1:6;
p,
q // a,
b
by A2, AFF_1:4;
then
LIN p,
q,
b
by A7, A10, AFF_1:9;
hence
contradiction
by A4, A7, A10, A9, AFF_1:8;
verum
end;
p,q // a,z
by A5, AFF_1:4;
then
a,b // a,z
by A2, A7, AFF_1:5;
then A12:
LIN a,b,z
by AFF_1:def 1;
a <> b
by A4, AFF_1:7;
then
( a = z or b = z )
by A1, A12;
hence
a,q // b,p
by A6, A11, AFF_1:4; verum