assume card X is empty ; :: thesis: contradiction
then ex f being Function st
( f is one-to-one & dom f = X & rng f = {} ) by Def2, WELLORD2:def 4;
hence contradiction by RELAT_1:42; :: thesis: verum