let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = b or not LIN x,a,b )

set A = Line (a,b);

assume that

A4: a <> b and

A5: LIN x,a,b ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = b or not LIN x,a,b )

set A = Line (a,b);

assume that

A4: a <> b and

A5: LIN x,a,b ; :: thesis: 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; :: thesis: verum