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