let seq, seq' be Real_Sequence; :: thesis: ( seq is convergent & seq' is convergent implies seq - seq' is convergent )
assume that
A1: seq is convergent and
A2: seq' is convergent ; :: thesis: seq - seq' is convergent
- seq' is convergent by A2, Th21;
hence seq - seq' is convergent by A1, Th19; :: thesis: verum