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