let seq1, seq2, seq3 be Real_Sequence; :: thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
thus seq1 - (seq2 - seq3) = seq1 + ((- seq2) - (- seq3)) by Th32
.= (seq1 - seq2) + seq3 by Th20 ; :: thesis: verum