let n be Nat; :: thesis: for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & r = 1 holds
|((Bn - Cn),(An - Bn))| = 0
let r be Real; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & r = 1 holds
|((Bn - Cn),(An - Bn))| = 0
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: ( Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & r = 1 implies |((Bn - Cn),(An - Bn))| = 0 )
assume that
A1: Bn <> Cn and
A2: r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) and
A3: r = 1 ; :: thesis: |((Bn - Cn),(An - Bn))| = 0
set A = An;
set B = Bn;
set C = Cn;
reconsider rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
A4: rB - rC <> 0* n by A1, EUCLIDLP:9;
1 * |((Bn - Cn),(Bn - Cn))| = (- (|((Cn - An),(Bn - Cn))| / |((Bn - Cn),(Bn - Cn))|)) * |((Bn - Cn),(Bn - Cn))| by A3, A2, Th13;
then |((Bn - Cn),(Bn - Cn))| = - ((|((Cn - An),(Bn - Cn))| / |((Bn - Cn),(Bn - Cn))|) * |((Bn - Cn),(Bn - Cn))|) ;
then |((Bn - Cn),(Bn - Cn))| = - |((Cn - An),(Bn - Cn))| by A4, EUCLID_4:17, XCMPLX_1:87;
hence |((Bn - Cn),(An - Bn))| = 0 by Th18; :: thesis: verum