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