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