take 1-sorted(# 1 #) ; :: thesis: ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty )
thus ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty ) by Def9, CARD_1:87; :: thesis: verum