let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: contradiction

A9: a9 <> b9

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

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; :: thesis: verum

b9 = x

let a, a9, b, b9, o, x be Element of AS; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: contradiction

A9: a9 <> b9

proof

then A11:
Line (a9,b9) is being_line
;
assume A10:
a9 = b9
; :: thesis: contradiction

then a9 = o by A1, A2, A3, Th53;

hence contradiction by A1, A4, A6, A8, A10, Th54; :: thesis: verum

end;then a9 = o by A1, A2, A3, Th53;

hence contradiction by A1, A4, A6, A8, A10, Th54; :: thesis: verum

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

proof

A24:
o in Line (o,a)
by Th14;
assume A23:
a9 = o
; :: thesis: contradiction

then b9 = o by A1, A3, A5, Th54;

hence contradiction by A1, A4, A6, A8, A23, Th54; :: thesis: verum

end;then b9 = o by A1, A3, A5, Th54;

hence contradiction by A1, A4, A6, A8, A23, Th54; :: thesis: verum

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; :: thesis: verum