let AFP be AffinPlane; :: thesis: for a, b, p, q, x, y being Element of AFP st a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p holds
( p <> q & LIN a,b,y )
let a, b, p, q, x, y be Element of AFP; :: thesis: ( a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p implies ( p <> q & LIN a,b,y ) )
assume that
A1: ( a <> b & LIN a,b,x ) and
A2: a,b // p,q and
A3: a,p // b,q and
A4: p,q // x,y and
A5: not LIN a,b,p ; :: thesis: ( p <> q & LIN a,b,y )
thus p <> q :: thesis: LIN a,b,y

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 A5, AFF_1:6; :: thesis: verum

end;

then a,b // x,y by A2, A4, AFF_1:5;
hence LIN a,b,y by A1, AFF_1:9; :: thesis: verum