let AS be AffinSpace; :: thesis: for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q holds
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
let a, b, c, p, q be Element of AS; :: thesis: ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )
assume that
A1: LIN a,b,c and
A2: a <> b and
A3: a <> c and
A4: b <> c and
A5: not LIN a,b,p and
A6: LIN a,b,q ; :: thesis: ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )

A7: now :: thesis: ( q = c & q <> a & q <> b implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )

assume that
A8: q = c and
q <> a and
q <> b ; :: thesis: ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )

A9: now :: thesis: not LIN q,a,p

assume A10: LIN q,a,p ; :: thesis: contradiction
( LIN c,a,b & LIN c,a,a ) by A1, AFF_1:6, AFF_1:7;
hence contradiction by A3, A5, A8, A10, AFF_1:8; :: thesis: verum

end;

LIN q,a,b by A6, AFF_1:6;
hence ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) by A2, A3, A4, A8, A9, Lm1; :: thesis: verum

end;

A11: now :: thesis: ( q <> a & q <> b & q <> c implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )

assume that
A12: q <> a and
A13: q <> b and
q <> c ; :: thesis: ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )

A14: now :: thesis: not LIN q,a,p

assume LIN q,a,p ; :: thesis: contradiction
then LIN a,q,p by AFF_1:6;
then A15: a,q // a,p by AFF_1:def 1;
LIN a,q,b by A6, AFF_1:6;
then a,q // a,b by AFF_1:def 1;
then a,b // a,p by A12, A15, AFF_1:5;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum

end;

LIN q,a,b by A6, AFF_1:6;
hence ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) by A2, A12, A13, A14, Lm1; :: thesis: verum

end;

now :: thesis: ( q = b & q <> a & q <> c implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )

assume that
A16: q = b and
q <> a and
q <> c ; :: thesis: ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
( LIN q,a,c & not LIN q,a,p ) by A1, A5, A16, AFF_1:6;
hence ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) by A2, A3, A4, A16, Lm1; :: thesis: verum

end;

hence ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) by A1, A2, A3, A4, A5, A7, A11, Lm1; :: thesis: verum