let X be set ; :: thesis: ( X, {} are_equipotent implies X = {} )
given f being Function such that f is one-to-one and
A1: ( dom f = X & rng f = {} ) ; :: according to WELLORD2:def 4 :: thesis: X = {}
thus X = {} by A1, RELAT_1:42; :: thesis: verum