theorem Th13: :: EUCLID13:14

for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds
( ((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)| = |((Cn - An),(Bn - Cn))| & |((Bn - Cn),(Bn - Cn))| + |((Cn - An),(Bn - Cn))| = |((Bn - Cn),(Bn - An))| )