dom C = I by PBOOLE:def 3;
hence C . i is TolStr by Def14; :: thesis: verum