let AS be AffinSpace; :: thesis: for a, b, c, p being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p holds
ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
let a, b, c, p be Element of AS; :: thesis: ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p implies ex x being Element of AS st
( LIN p,a,x & p <> x & a <> 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 ; :: thesis: ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
a,b // a,c by A1, AFF_1:def 1;
then b,a // a,c by AFF_1:4;
then consider x being Element of AS such that
A6: p,a // a,x and
A7: p,b // c,x by A2, DIRAF:40;

A8: now :: thesis: not p = x

assume p = x ; :: thesis: contradiction
then p,b // p,c by A7, AFF_1:4;
then LIN p,b,c by AFF_1:def 1;
then A9: LIN b,c,p by AFF_1:6;
( LIN b,c,a & LIN b,c,b ) by A1, AFF_1:6, AFF_1:7;
hence contradiction by A4, A5, A9, AFF_1:8; :: thesis: verum

end;

A10: now :: thesis: not a = x

assume a = x ; :: thesis: contradiction
then A11: p,b // a,c by A7, AFF_1:4;
a,b // a,c by A1, AFF_1:def 1;
then a,b // p,b by A3, A11, AFF_1:5;
then b,a // b,p by AFF_1:4;
then LIN b,a,p by AFF_1:def 1;
hence contradiction by A5, AFF_1:6; :: thesis: verum

end;

a,p // a,x by A6, AFF_1:4;
then LIN a,p,x by AFF_1:def 1;
then LIN p,a,x by AFF_1:6;
hence ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x ) by A8, A10; :: thesis: verum