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