dom C = I by PBOOLE:def 3;
then C . i in rng C by FUNCT_1:12;
hence C . i is pcs-tol-symmetric TolStr by Def18; :: thesis: verum