take 1-sorted(# 1 #) ; :: thesis: ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict )
thus ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict ) by CARD_1:49; :: thesis: verum