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
proof
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;
A8: a <> q
proof
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;
A9: not LIN a,b,q
proof
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;
consider r being Element of AS such that
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;
A18: now :: thesis: ( p = r implies ex x being Element of AS st
( 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
proof
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;
assume A22: p = r ; :: thesis: ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
A23: now :: thesis: not p = s
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;
a,b // q,s by A19, AFF_1:4;
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;
q <> r
proof
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;
hence ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) by A15, A18; :: thesis: verum