let X be trivial set ; :: thesis: for Y being set st X,Y are_equipotent holds
Y is trivial
let Y be set ; :: thesis: ( X,Y are_equipotent implies Y is trivial )
assume A1: X,Y are_equipotent ; :: thesis: Y is trivial
A2: card X < 2 by NAT_D:60;
A3: Y is finite by A1, CARD_1:38;
card X = card Y by A1, CARD_1:5;
hence Y is trivial by A2, A3, NAT_D:60; :: thesis: verum