let AFP be AffinPlane; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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

proof

assume p = q ; :: thesis: contradiction
then p,a // p,b by A3, AFF_1:4;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A4, AFF_1:6; :: thesis: verum

end;

A8: not LIN a,p,q

proof

A9: LIN p,q,p by AFF_1:7;
assume LIN a,p,q ; :: thesis: 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; :: thesis: verum

end;

A11: now

assume a = z ; :: thesis: contradiction
then a,p // a,q by A6, AFF_1:4;
hence contradiction by A8, AFF_1:def 1; :: thesis: 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; :: thesis: verum