let seq be sequence of (REAL-US n); :: according to BHSP_3:def 4 :: thesis: ( not seq is Cauchy or seq is convergent )

reconsider seq9 = seq as sequence of (REAL-NS n) by Th15;

assume seq is Cauchy ; :: thesis: seq is convergent

then seq9 is convergent by Th12, Th18;

hence seq is convergent by Th16; :: thesis: verum

reconsider seq9 = seq as sequence of (REAL-NS n) by Th15;

assume seq is Cauchy ; :: thesis: seq is convergent

then seq9 is convergent by Th12, Th18;

hence seq is convergent by Th16; :: thesis: verum