let AS be AffinSpace; for a, a9, b, b9, o, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds
b9 = x
let a, a9, b, b9, o, x be Element of AS; ( not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x implies b9 = x )
assume that
A1:
not LIN o,a,b
and
A2:
LIN o,a,a9
and
A3:
LIN o,b,b9
and
A4:
LIN o,b,x
and
A5:
a,b // a9,b9
and
A6:
a,b // a9,x
; b9 = x
set A = Line (o,a);
set C = Line (o,b);
set P = Line (a9,b9);
A7:
a9 in Line (a9,b9)
by Th14;
assume A8:
b9 <> x
; contradiction
A9:
a9 <> b9
then A11:
Line (a9,b9) is being_line
;
A12:
o <> b
by A1, Th6;
then A13:
Line (o,b) is being_line
;
A14:
b9 in Line (a9,b9)
by Th14;
a <> b
by A1, Th6;
then
a9,b9 // a9,x
by A5, A6, Th4;
then
LIN a9,b9,x
;
then A15:
x in Line (a9,b9)
by A9, A11, A7, A14, Th24;
A16:
b in Line (o,b)
by Th14;
A17:
o in Line (o,b)
by Th14;
then A18:
x in Line (o,b)
by A4, A12, A13, A16, Th24;
b9 in Line (o,b)
by A3, A12, A13, A17, A16, Th24;
then A19:
a9 in Line (o,b)
by A8, A13, A11, A7, A14, A18, A15, Th17;
A20:
o <> a
by A1, Th6;
then A21:
Line (o,a) is being_line
;
A22:
a9 <> o
A24:
o in Line (o,a)
by Th14;
A25:
a in Line (o,a)
by Th14;
then
a9 in Line (o,a)
by A2, A20, A21, A24, Th24;
then
b in Line (o,a)
by A22, A21, A13, A24, A17, A16, A19, Th17;
hence
contradiction
by A1, A21, A24, A25, Th20; verum