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

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