theorem
proved
ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1
show as:
ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1