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