take PrefStr(# {},({} ({},{})) #) ; :: thesis: ( PrefStr(# {},({} ({},{})) #) is empty & PrefStr(# {},({} ({},{})) #) is strict )
thus ( PrefStr(# {},({} ({},{})) #) is empty & PrefStr(# {},({} ({},{})) #) is strict ) ; :: thesis: verum