let AFP be AffinPlane; :: thesis: for a, b, y being Element of AFP st a <> b holds
ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
let a, b, y be Element of AFP; :: thesis: ( a <> b implies ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) )
assume A1: a <> b ; :: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )

A2: now :: thesis: ( LIN a,b,y implies ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) )

assume A3: LIN a,b,y ; :: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
consider p being Element of AFP such that
A4: not LIN a,b,p by A1, AFF_1:13;
consider q being Element of AFP such that
A5: a,b // p,q and
A6: a,p // b,q by DIRAF:40;

A7: now :: thesis: not p = q

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

end;

consider x being Element of AFP such that
A8: q,p // y,x and
A9: q,y // p,x by DIRAF:40;
A10: p,x // q,y by A9, AFF_1:4;
A11: p,q // x,y by A8, AFF_1:4;
then ( a,b // x,y or p = q ) by A5, AFF_1:5;
then a,b // y,x by A7, AFF_1:4;
then LIN a,b,x by A1, A3, AFF_1:9;
hence ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) by A4, A5, A6, A11, A10; :: thesis: verum

end;

now :: thesis: ( not LIN a,b,y implies ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) )

consider x being Element of AFP such that
A12: ( b,a // y,x & b,y // a,x ) by DIRAF:40;
A13: ( a,b // x,y & a,x // b,y ) by A12, AFF_1:4;
assume not LIN a,b,y ; :: thesis: ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
then not LIN b,a,y by AFF_1:6;
then not LIN a,b,x by A12, Lm5;
hence ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) by A13; :: thesis: verum

end;

hence ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) ) by A2; :: thesis: verum