theorem
proved
reducedCellularToOrdinary_comp_ordinaryCellularToReduced
show as:
reducedCellularToOrdinary_comp_ordinaryCellularToReduced