let AS be AffinSpace; 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; 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; ( 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
; 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
; 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; verum