let n be Nat; :: thesis: for r being Real
for An, Bn, Cn, Dn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & Dn = (r * Bn) + ((1 - r) * Cn) holds
|((Dn - An),(Dn - Cn))| = 0
let r be Real; :: thesis: for An, Bn, Cn, Dn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & Dn = (r * Bn) + ((1 - r) * Cn) holds
|((Dn - An),(Dn - Cn))| = 0
let An, Bn, Cn, Dn be Point of (TOP-REAL n); :: thesis: ( Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & Dn = (r * Bn) + ((1 - r) * Cn) implies |((Dn - An),(Dn - Cn))| = 0 )
assume that
A1: Bn <> Cn and
A2: r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) and
A3: Dn = (r * Bn) + ((1 - r) * Cn) ; :: thesis: |((Dn - An),(Dn - Cn))| = 0
reconsider rA = An, rB = Bn, rC = Cn, rD = Dn as Element of REAL n by EUCLID:22;
reconsider rrB = r * rB, rrC = (1 - r) * rC as Element of REAL n ;
A4: |(rrB,rrB)| = r * |(rB,rrB)| by EUCLID_4:21
.= r * (r * |(rB,rB)|) by EUCLID_4:22
.= (r * r) * |(rB,rB)| ;
A5: |(rrB,rrC)| = r * |(rB,rrC)| by EUCLID_4:21
.= r * ((1 - r) * |(rB,rC)|) by EUCLID_4:22
.= (r * (1 - r)) * |(rB,rC)| ;
A6: |(rrC,rrC)| = (1 - r) * |(rC,rrC)| by EUCLID_4:21
.= (1 - r) * ((1 - r) * |(rC,rC)|) by EUCLID_4:22
.= ((1 - r) * (1 - r)) * |(rC,rC)| ;
A7: |(rD,rD)| = (|(rrB,rrB)| + (2 * |(rrB,rrC)|)) + |(rrC,rrC)| by A3, RVSUM_1:138
.= (((r * r) * |(rB,rB)|) + (((2 * r) * (1 - r)) * |(rB,rC)|)) + (((1 - r) * (1 - r)) * |(rC,rC)|) by A4, A5, A6 ;
A8: |(rD,rC)| = |(rrB,rC)| + |(rrC,rC)| by A3, EUCLID_4:20
.= (r * |(rB,rC)|) + |(rrC,rC)| by EUCLID_4:21
.= (r * |(rB,rC)|) + ((1 - r) * |(rC,rC)|) by EUCLID_4:21 ;
A9: |(rA,rD)| = |(rA,rrB)| + |(rA,rrC)| by A3, EUCLID_4:28
.= (r * |(rA,rB)|) + |(rA,rrC)| by EUCLID_4:22
.= (r * |(rA,rB)|) + ((1 - r) * |(rA,rC)|) by EUCLID_4:22 ;
A10: (|(rB,rB)| - (2 * |(rB,rC)|)) + |(rC,rC)| = |((rB - rC),(rB - rC))| by RVSUM_1:139;
A11: rB - rC <> 0* n by A1, EUCLIDLP:9;
A12: ((((r * |((rB - rC),(rB - rC))|) + |(rB,rC)|) - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)| = ((((- (((((|(rB,rC)| - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)|) / |((rB - rC),(rB - rC))|) * |((rB - rC),(rB - rC))|)) + |(rB,rC)|) - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)| by A2
.= ((((- (((|(rB,rC)| - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)|)) + |(rB,rC)|) - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)| by A11, EUCLID_4:17, XCMPLX_1:87
.= 0 ;
|((rD - rA),(rD - rC))| = (((((((r * r) * |(rB,rB)|) + ((2 * r) * |(rB,rC)|)) - (((2 * r) * r) * |(rB,rC)|)) + ((|(rC,rC)| - ((2 * r) * |(rC,rC)|)) + ((r * r) * |(rC,rC)|))) - ((r * |(rB,rC)|) + ((1 - r) * |(rC,rC)|))) - ((r * |(rA,rB)|) + ((1 - r) * |(rA,rC)|))) + |(rA,rC)| by A9, A7, A8, RVSUM_1:137
.= r * (((((((r * |(rB,rB)|) + |(rB,rC)|) - ((2 * r) * |(rB,rC)|)) + (r * |(rC,rC)|)) - |(rC,rC)|) - |(rA,rB)|) + |(rA,rC)|)
.= 0 by A10, A12 ;
hence |((Dn - An),(Dn - Cn))| = 0 ; :: thesis: verum