let AS be AffinSpace; :: thesis: ( ex a, b, c being Element of AS st
( LIN a,b,c & a <> b & a <> c & b <> c ) implies for p, q being Element of AS ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )
given a, b, c being Element of AS such that A1: LIN a,b,c and
A2: a <> b and
A3: a <> c and
A4: b <> c ; :: thesis: for p, q being Element of AS ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
let p, q be Element of AS; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )

A5: now :: thesis: ( LIN a,b,p & LIN a,b,q implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume that
A6: LIN a,b,p and
A7: LIN a,b,q ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
A8: LIN a,b,b by AFF_1:7;
A9: LIN a,b,a by AFF_1:7;

now :: thesis: ( ( p = c or q = c ) implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume A10: ( p = c or q = c ) ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )

now :: thesis: ( ( p <> a or q <> b ) implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume ( p <> a or q <> b ) ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )

A11: now :: thesis: ( p = c & p <> a implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume that
A12: p = c and
A13: p <> a ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
( q = b implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) ) by A1, A2, A9, A8, A12, A13, AFF_1:8;
hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A2, A4, A7, A8, A12, AFF_1:8; :: thesis: verum

end;

now :: thesis: ( q = c & q <> b implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume that
A14: q = c and
q <> b ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
( p = b implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) ) by A1, A2, A3, A9, A8, A14, AFF_1:8;
hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A2, A4, A6, A8, A14, AFF_1:8; :: thesis: verum

end;

hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A3, A4, A10, A11; :: thesis: verum

end;

hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A3, A4; :: thesis: verum

end;

hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A2, A6, A7, AFF_1:8; :: thesis: verum

end;

A15: now :: thesis: ( not LIN a,b,p & not LIN a,b,q implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume that
A16: not LIN a,b,p and
not LIN a,b,q ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )

now :: thesis: ( not p,q // a,b implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

consider p9 being Element of AS such that
A17: a,b // p,p9 and
A18: p <> p9 by DIRAF:40;
assume A19: not p,q // a,b ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
A20: not LIN p,p9,q

proof

assume LIN p,p9,q ; :: thesis: contradiction
then p,p9 // p,q by AFF_1:def 1;
hence contradiction by A19, A17, A18, AFF_1:5; :: thesis: verum

end;

p,p9 // a,b by A17, AFF_1:4;
then ex p99 being Element of AS st
( LIN p,p9,p99 & p <> p99 & p9 <> p99 ) by A1, A2, A3, A4, A16, Lm3;
then consider r being Element of AS such that
A21: LIN q,p,r and
A22: ( q <> r & p <> r ) by A18, A20, Lm1;
LIN p,q,r by A21, AFF_1:6;
hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A22; :: thesis: verum

end;

hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A16, Lm3; :: thesis: verum

end;

now :: thesis: ( not LIN a,b,q & LIN a,b,p implies ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) )

assume ( not LIN a,b,q & LIN a,b,p ) ; :: thesis: ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
then consider x being Element of AS such that
A23: LIN q,p,x and
A24: ( q <> x & p <> x ) by A1, A2, A3, A4, Lm2;
LIN p,q,x by A23, AFF_1:6;
hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A24; :: thesis: verum

end;

hence ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A5, A15, Lm2; :: thesis: verum