for X being trivial set
for Y being set st X,Y are_equipotent holds
Y is trivial