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