theorem :: BCIALG_4:4

canceled;