consider R being TolStr ;
take I --> R ; :: thesis: I --> R is TolStr-yielding
thus I --> R is TolStr-yielding ; :: thesis: verum