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