let AS be AffinSpace; ( 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
; 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; ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )
A5:
now ( 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
;
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 ( ( 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 )
;
ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )now ( ( 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 )
;
ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )A11:
now ( 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
;
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;
verum end; now ( 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
;
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;
verum end; hence
ex
r being
Element of
AS st
(
LIN p,
q,
r &
p <> r &
q <> r )
by A3, A4, A10, A11;
verum end; hence
ex
r being
Element of
AS st
(
LIN p,
q,
r &
p <> r &
q <> r )
by A1, A3, A4;
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;
verum end;
A15:
now ( 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
;
ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )now ( 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
;
ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )A20:
not
LIN p,
p9,
q
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;
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;
verum end;
now ( 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 )
;
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;
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; verum