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;
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

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