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 & a,p // b,q & not LIN a,b,p ) ; :: thesis: a,q // b,p
A3: ( a <> b & a <> p & b <> p ) by A2, AFF_1:16;
A4: p <> q

proof

assume p = q ; :: thesis: contradiction
then p,a // p,b by A2, AFF_1:13;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A2, AFF_1:15; :: thesis: verum

end;

A5: not LIN a,p,q

proof

assume LIN a,p,q ; :: thesis: contradiction
then ( LIN p,q,a & p,q // a,b ) by A2, AFF_1:13, AFF_1:15;
then ( LIN p,q,b & LIN p,q,a & LIN p,q,p ) by A4, AFF_1:16, AFF_1:18;
hence contradiction by A2, A4, AFF_1:17; :: thesis: verum

end;

consider z being Element of AFP such that
A6: ( q,p // a,z & q,a // p,z ) by DIRAF:47;
p,q // a,z by A6, AFF_1:13;
then a,b // a,z by A2, A4, AFF_1:14;
then LIN a,b,z by AFF_1:def 1;
then A7: ( a = z or b = z ) by A1, A3;

now

assume a = z ; :: thesis: contradiction
then a,p // a,q by A6, AFF_1:13;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum

end;

hence a,q // b,p by A6, A7, AFF_1:13; :: thesis: verum