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;

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

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

A10: now :: thesis: not a = x

a,p // a,x
by A6, AFF_1:4;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;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

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