let AS be AffinSpace; for a, b, c, p being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p holds
ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
let a, b, c, p be Element of AS; ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p implies ex x being Element of AS st
( LIN p,a,x & p <> x & a <> 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
; ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
a,b // a,c
by A1, AFF_1:def 1;
then
b,a // a,c
by AFF_1:4;
then consider x being Element of AS such that
A6:
p,a // a,x
and
A7:
p,b // c,x
by A2, DIRAF:40;
A8:
now not p = xassume
p = x
;
contradictionthen
p,
b // p,
c
by A7, AFF_1:4;
then
LIN p,
b,
c
by AFF_1:def 1;
then A9:
LIN b,
c,
p
by AFF_1:6;
(
LIN b,
c,
a &
LIN b,
c,
b )
by A1, AFF_1:6, AFF_1:7;
hence
contradiction
by A4, A5, A9, AFF_1:8;
verum end;
A10:
now not a = xassume
a = x
;
contradictionthen A11:
p,
b // a,
c
by A7, AFF_1:4;
a,
b // a,
c
by A1, AFF_1:def 1;
then
a,
b // p,
b
by A3, A11, AFF_1:5;
then
b,
a // b,
p
by AFF_1:4;
then
LIN b,
a,
p
by AFF_1:def 1;
hence
contradiction
by A5, AFF_1:6;
verum end;
a,p // a,x
by A6, AFF_1:4;
then
LIN a,p,x
by AFF_1:def 1;
then
LIN p,a,x
by AFF_1:6;
hence
ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
by A8, A10; verum