let AS be AffinSpace; 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 & LIN a,b,q 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; ( LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q 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:
LIN a,b,q
; ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
A7:
now ( q = c & q <> a & q <> b implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )assume that A8:
q = c
and
q <> a
and
q <> b
;
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )A9:
now not LIN q,a,passume A10:
LIN q,
a,
p
;
contradiction
(
LIN c,
a,
b &
LIN c,
a,
a )
by A1, AFF_1:6, AFF_1:7;
hence
contradiction
by A3, A5, A8, A10, AFF_1:8;
verum end;
LIN q,
a,
b
by A6, AFF_1:6;
hence
ex
x being
Element of
AS st
(
LIN p,
q,
x &
p <> x &
q <> x )
by A2, A3, A4, A8, A9, Lm1;
verum end;
A11:
now ( q <> a & q <> b & q <> c implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )assume that A12:
q <> a
and A13:
q <> b
and
q <> c
;
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )A14:
now not LIN q,a,passume
LIN q,
a,
p
;
contradictionthen
LIN a,
q,
p
by AFF_1:6;
then A15:
a,
q // a,
p
by AFF_1:def 1;
LIN a,
q,
b
by A6, AFF_1:6;
then
a,
q // a,
b
by AFF_1:def 1;
then
a,
b // a,
p
by A12, A15, AFF_1:5;
hence
contradiction
by A5, AFF_1:def 1;
verum end;
LIN q,
a,
b
by A6, AFF_1:6;
hence
ex
x being
Element of
AS st
(
LIN p,
q,
x &
p <> x &
q <> x )
by A2, A12, A13, A14, Lm1;
verum end;
now ( q = b & q <> a & q <> c implies ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x ) )assume that A16:
q = b
and
q <> a
and
q <> c
;
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
(
LIN q,
a,
c & not
LIN q,
a,
p )
by A1, A5, A16, AFF_1:6;
hence
ex
x being
Element of
AS st
(
LIN p,
q,
x &
p <> x &
q <> x )
by A2, A3, A4, A16, Lm1;
verum end;
hence
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
by A1, A2, A3, A4, A5, A7, A11, Lm1; verum