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 & p,q // a,b 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 & p,q // a,b 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: p,q // a,b ; :: thesis: ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x )

A7: b <> q

A13: b,c // q,r and

A14: b,q // c,r by DIRAF:40;

LIN b,a,c by A1, AFF_1:6;

then b,a // b,c by AFF_1:def 1;

then b,a // q,r by A4, A13, AFF_1:5;

then a,b // q,r by AFF_1:4;

then p,q // q,r by A2, A6, AFF_1:5;

then q,p // q,r by AFF_1:4;

then LIN q,p,r by AFF_1:def 1;

then A15: LIN p,q,r by AFF_1:6;

A16: not LIN a,c,p

( LIN p,q,x & p <> x & q <> x ) by A15, A18; :: thesis: verum

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 & p,q // a,b 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: p,q // a,b ; :: thesis: ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x )

A7: b <> q

proof

A8:
a <> q
assume
b = q
; :: thesis: contradiction

then b,p // b,a by A6, AFF_1:4;

then LIN b,p,a by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

end;then b,p // b,a by A6, AFF_1:4;

then LIN b,p,a by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

proof

A9:
not LIN a,b,q
assume
a = q
; :: thesis: contradiction

then a,p // a,b by A6, AFF_1:4;

then LIN a,p,b by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

end;then a,p // a,b by A6, AFF_1:4;

then LIN a,p,b by AFF_1:def 1;

hence contradiction by A5, AFF_1:6; :: thesis: verum

proof

consider r being Element of AS such that
assume A10:
LIN a,b,q
; :: thesis: contradiction

then a,b // a,q by AFF_1:def 1;

then p,q // a,q by A2, A6, AFF_1:5;

then q,p // q,a by AFF_1:4;

then LIN q,p,a by AFF_1:def 1;

then A11: LIN q,a,p by AFF_1:6;

A12: LIN q,a,a by AFF_1:7;

LIN q,a,b by A10, AFF_1:6;

hence contradiction by A5, A8, A11, A12, AFF_1:8; :: thesis: verum

end;then a,b // a,q by AFF_1:def 1;

then p,q // a,q by A2, A6, AFF_1:5;

then q,p // q,a by AFF_1:4;

then LIN q,p,a by AFF_1:def 1;

then A11: LIN q,a,p by AFF_1:6;

A12: LIN q,a,a by AFF_1:7;

LIN q,a,b by A10, AFF_1:6;

hence contradiction by A5, A8, A11, A12, AFF_1:8; :: thesis: verum

A13: b,c // q,r and

A14: b,q // c,r by DIRAF:40;

LIN b,a,c by A1, AFF_1:6;

then b,a // b,c by AFF_1:def 1;

then b,a // q,r by A4, A13, AFF_1:5;

then a,b // q,r by AFF_1:4;

then p,q // q,r by A2, A6, AFF_1:5;

then q,p // q,r by AFF_1:4;

then LIN q,p,r by AFF_1:def 1;

then A15: LIN p,q,r by AFF_1:6;

A16: not LIN a,c,p

proof

assume A17:
LIN a,c,p
; :: thesis: contradiction

( LIN a,c,b & LIN a,c,a ) by A1, AFF_1:6, AFF_1:7;

hence contradiction by A3, A5, A17, AFF_1:8; :: thesis: verum

end;( LIN a,c,b & LIN a,c,a ) by A1, AFF_1:6, AFF_1:7;

hence contradiction by A3, A5, A17, AFF_1:8; :: thesis: verum

A18: now :: thesis: ( p = r implies ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x ) )

q <> r
( LIN p,q,x & p <> x & q <> x ) )

consider s being Element of AS such that

A19: b,a // q,s and

A20: b,q // a,s by DIRAF:40;

A21: q <> s

( LIN p,q,x & p <> x & q <> x )

then p,q // q,s by A2, A6, AFF_1:5;

then q,p // q,s by AFF_1:4;

then LIN q,p,s by AFF_1:def 1;

then LIN p,q,s by AFF_1:6;

hence ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x ) by A23, A21; :: thesis: verum

end;A19: b,a // q,s and

A20: b,q // a,s by DIRAF:40;

A21: q <> s

proof

assume A22:
p = r
; :: thesis: ex x being Element of AS st
assume
q = s
; :: thesis: contradiction

then q,b // q,a by A20, AFF_1:4;

then LIN q,b,a by AFF_1:def 1;

hence contradiction by A9, AFF_1:6; :: thesis: verum

end;then q,b // q,a by A20, AFF_1:4;

then LIN q,b,a by AFF_1:def 1;

hence contradiction by A9, AFF_1:6; :: thesis: verum

( LIN p,q,x & p <> x & q <> x )

A23: now :: thesis: not p = s

a,b // q,s
by A19, AFF_1:4;assume
p = s
; :: thesis: contradiction

then a,p // c,p by A7, A14, A22, A20, AFF_1:5;

then p,a // p,c by AFF_1:4;

then LIN p,a,c by AFF_1:def 1;

hence contradiction by A16, AFF_1:6; :: thesis: verum

end;then a,p // c,p by A7, A14, A22, A20, AFF_1:5;

then p,a // p,c by AFF_1:4;

then LIN p,a,c by AFF_1:def 1;

hence contradiction by A16, AFF_1:6; :: thesis: verum

then p,q // q,s by A2, A6, AFF_1:5;

then q,p // q,s by AFF_1:4;

then LIN q,p,s by AFF_1:def 1;

then LIN p,q,s by AFF_1:6;

hence ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x ) by A23, A21; :: thesis: verum

proof

hence
ex x being Element of AS st
assume
q = r
; :: thesis: contradiction

then q,b // q,c by A14, AFF_1:4;

then LIN q,b,c by AFF_1:def 1;

then A24: LIN b,c,q by AFF_1:6;

( LIN b,c,a & LIN b,c,b ) by A1, AFF_1:6, AFF_1:7;

hence contradiction by A4, A9, A24, AFF_1:8; :: thesis: verum

end;then q,b // q,c by A14, AFF_1:4;

then LIN q,b,c by AFF_1:def 1;

then A24: LIN b,c,q by AFF_1:6;

( LIN b,c,a & LIN b,c,b ) by A1, AFF_1:6, AFF_1:7;

hence contradiction by A4, A9, A24, AFF_1:8; :: thesis: verum

( LIN p,q,x & p <> x & q <> x ) by A15, A18; :: thesis: verum