assume A1: not <*c*> is non-empty ; :: thesis: contradiction
rng <*c*> = {c} by FINSEQ_1:38;
hence contradiction by A1; :: thesis: verum