take emptyTolStr ; :: thesis: emptyTolStr is empty
thus emptyTolStr is empty ; :: thesis: verum