let x, X, Y be set ; :: thesis: ( x in X & X,Y are_equipotent implies ( Y <> {} & ex x being set st x in Y ) )
assume A1: x in X ; :: thesis: ( not X,Y are_equipotent or ( Y <> {} & ex x being set st x in Y ) )
given f being Function such that A2: ( f is one-to-one & dom f = X & rng f = Y ) ; :: according to WELLORD2:def 4 :: thesis: ( Y <> {} & ex x being set st x in Y )
f . x in Y by A1, A2, FUNCT_1:def 5;
hence Y <> {} ; :: thesis: ex x being set st x in Y
take f . x ; :: thesis: f . x in Y
thus f . x in Y by A1, A2, FUNCT_1:def 5; :: thesis: verum