let AS be AffinSpace; :: thesis: for a, a9, b, b9, p being Element of AS

for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

let a, a9, b, b9, p be Element of AS; :: thesis: for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

let K be Subset of AS; :: thesis: ( a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b implies a9 = b9 )

assume that

A1: a9,b9 // K and

A2: LIN p,a,a9 and

A3: LIN p,b,b9 and

A4: p in K and

A5: not a in K and

A6: a = b ; :: thesis: a9 = b9

set A = Line (p,a);

A7: b9 in Line (p,a) by A3, A6, Def2;

A8: p in Line (p,a) by Th14;

A9: a9 in Line (p,a) by A2, Def2;

assume A10: a9 <> b9 ; :: thesis: contradiction

Line (p,a) is being_line by A4, A5;

then Line (p,a) = Line (a9,b9) by A9, A7, A10, Lm6;

then Line (p,a) // K by A1, A10;

then Line (p,a) = K by A4, A8, Th44;

hence contradiction by A5, Th14; :: thesis: verum

for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

let a, a9, b, b9, p be Element of AS; :: thesis: for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds

a9 = b9

let K be Subset of AS; :: thesis: ( a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b implies a9 = b9 )

assume that

A1: a9,b9 // K and

A2: LIN p,a,a9 and

A3: LIN p,b,b9 and

A4: p in K and

A5: not a in K and

A6: a = b ; :: thesis: a9 = b9

set A = Line (p,a);

A7: b9 in Line (p,a) by A3, A6, Def2;

A8: p in Line (p,a) by Th14;

A9: a9 in Line (p,a) by A2, Def2;

assume A10: a9 <> b9 ; :: thesis: contradiction

Line (p,a) is being_line by A4, A5;

then Line (p,a) = Line (a9,b9) by A9, A7, A10, Lm6;

then Line (p,a) // K by A1, A10;

then Line (p,a) = K by A4, A8, Th44;

hence contradiction by A5, Th14; :: thesis: verum