set R = the TolStr ;
take I --> the TolStr ; :: thesis: I --> the TolStr is ()
thus I --> the TolStr is () ; :: thesis: verum