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