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 )

( LIN p,q,x & p <> x & q <> x ) by A1, A2, A3, A4, A5, A7, A11, Lm1; :: 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 & 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 ) )

( 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 )

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

LIN q,a,b
by A6, AFF_1:6;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 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

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

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

( 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 )

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

LIN q,a,b
by A6, AFF_1:6;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;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

hence ex x being Element of AS st

( LIN p,q,x & p <> x & q <> x ) by A2, A12, A13, A14, Lm1; :: thesis: verum

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

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

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

( LIN p,q,x & p <> x & q <> x ) by A1, A2, A3, A4, A5, A7, A11, Lm1; :: thesis: verum