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 )

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A5, A15, Lm2; :: thesis: verum

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

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

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A6, A7, AFF_1:8; :: thesis: verum

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

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

( LIN p,q,r & p <> r & q <> r ) by A1, A3, A4; :: thesis: verum

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

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

( LIN p,q,r & p <> r & q <> r ) by A3, A4, A10, A11; :: thesis: verum

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

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

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

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

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

( LIN p,q,r & p <> r & q <> r ) by A3, A4, A10, A11; :: thesis: verum

( LIN p,q,r & p <> r & q <> r ) by A1, A3, A4; :: thesis: verum

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A6, A7, AFF_1:8; :: thesis: verum

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

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

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A16, Lm3; :: thesis: verum

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

hence
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

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

p,p9 // a,b
by A17, AFF_1:4;
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;then p,p9 // p,q by AFF_1:def 1;

hence contradiction by A19, A17, A18, AFF_1:5; :: thesis: verum

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

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A16, Lm3; :: thesis: verum

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

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

( LIN p,q,r & p <> r & q <> r ) by A1, A2, A3, A4, A5, A15, Lm2; :: thesis: verum