take 1-sorted(# {{}} #) ; :: thesis: ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty )
thus ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty ) ; :: thesis: verum