take emptyTolStr ; :: thesis: ( emptyTolStr is empty & emptyTolStr is strict )
thus ( emptyTolStr is empty & emptyTolStr is strict ) ; :: thesis: verum