take N-Str(# 1,f #) ; :: thesis: ( not N-Str(# 1,f #) is empty & N-Str(# 1,f #) is strict )
thus ( not N-Str(# 1,f #) is empty & N-Str(# 1,f #) is strict ) ; :: thesis: verum