let AS be AffinSpace; :: thesis: for x, a, b 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 x, a, b 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, Th15;
then A6: x in Line (a,b) by Def2;
A7: a in Line (a,b) by Th26;
Line (a,b) // K by A3, A4, Def5;
hence contradiction by A1, A2, A6, A7, Th59; :: thesis: verum