let X be RealUnitarySpace; :: thesis: for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
let seq1, seq2, seq3 be sequence of X; :: thesis: ( seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3 )
assume that
A1: seq1 is_compared_to seq2 and
A2: seq2 is_compared_to seq3 ; :: thesis: seq1 is_compared_to seq3
let r be Real; :: according to BHSP_3:def 2 :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq3 . n) < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq3 . n) < r
then A3: r / 2 > 0 by XREAL_1:217;
then consider m1 being Element of NAT such that
A4: for n being Element of NAT st n >= m1 holds
dist (seq1 . n),(seq2 . n) < r / 2 by A1, Def2;
consider m2 being Element of NAT such that
A5: for n being Element of NAT st n >= m2 holds
dist (seq2 . n),(seq3 . n) < r / 2 by A2, A3, Def2;
take m = m1 + m2; :: thesis: for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq3 . n) < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq1 . n),(seq3 . n) < r )
assume A6: n >= m ; :: thesis: dist (seq1 . n),(seq3 . n) < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A6, XXREAL_0:2;
then A7: dist (seq1 . n),(seq2 . n) < r / 2 by A4;
m >= m2 by NAT_1:12;
then n >= m2 by A6, XXREAL_0:2;
then dist (seq2 . n),(seq3 . n) < r / 2 by A5;
then A8: (dist (seq1 . n),(seq2 . n)) + (dist (seq2 . n),(seq3 . n)) < (r / 2) + (r / 2) by A7, XREAL_1:10;
dist (seq1 . n),(seq3 . n) <= (dist (seq1 . n),(seq2 . n)) + (dist (seq2 . n),(seq3 . n)) by BHSP_1:42;
hence dist (seq1 . n),(seq3 . n) < r by A8, XXREAL_0:2; :: thesis: verum