let AS be AffinSpace; for a, b, x being Element of AS
for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b
let a, b, x be Element of AS; for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds
not LIN x,a,b
let K be Subset of AS; ( x in K & not a in K & a,b // K & not a = b implies not LIN x,a,b )
assume that
A1:
x in K
and
A2:
not a in K
and
A3:
a,b // K
; ( a = b or not LIN x,a,b )
set A = Line (a,b);
assume that
A4:
a <> b
and
A5:
LIN x,a,b
; contradiction
LIN a,b,x
by A5, Th5;
then A6:
x in Line (a,b)
by Def2;
A7:
a in Line (a,b)
by Th14;
Line (a,b) // K
by A3, A4;
hence
contradiction
by A1, A2, A6, A7, Th44; verum