let AS be AffinSpace; :: thesis: for a', b', p, a, b being Element of
for K being Subset of st a',b' // K & LIN p,a,a' & LIN p,b,b' & p in K & not a in K & a = b holds
a' = b'
let a', b', p, a, b be Element of ; :: thesis: for K being Subset of st a',b' // K & LIN p,a,a' & LIN p,b,b' & p in K & not a in K & a = b holds
a' = b'
let K be Subset of ; :: thesis: ( a',b' // K & LIN p,a,a' & LIN p,b,b' & p in K & not a in K & a = b implies a' = b' )
assume that
A1: a',b' // K and
A2: LIN p,a,a' and
A3: LIN p,b,b' and
A4: p in K and
A5: not a in K and
A6: a = b ; :: thesis: a' = b'
set A = Line p,a;
A7: b' in Line p,a by A3, A6, Def2;
A8: p in Line p,a by Th26;
A9: a' in Line p,a by A2, Def2;
assume A10: a' <> b' ; :: thesis: contradiction
Line p,a is being_line by A4, A5, Def3;
then Line p,a = Line a',b' by A9, A7, A10, Lm6;
then Line p,a // K by A1, A10, Def5;
then Line p,a = K by A4, A8, Th59;
hence contradiction by A5, Th26; :: thesis: verum