for X being set st X, {} are_equipotent holds
X = {} by RELAT_1:42;