thus Triangle 2 = 1 + 2 by RVSUM_1:77, FINSEQ_2:52
.= 3 ; :: thesis: verum