theorem :: ALGSEQ_1:3

canceled;