let AS be AffinSpace; for a, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds
b = b9
let a, b, b9, o be Element of AS; ( not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b = b9 )
assume that
A1:
not LIN o,a,b
and
A2:
LIN o,b,b9
and
A3:
a,b // a,b9
; b = b9
LIN a,b,b9
by A3;
then A4:
LIN b,b9,a
by Th5;
A5:
LIN b,b9,b
by Th6;
assume A6:
b <> b9
; contradiction
LIN b,b9,o
by A2, Th5;
hence
contradiction
by A1, A6, A4, A5, Th7; verum