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 ) by Def11; :: thesis: verum