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