let P be IndexedPartition of X; :: thesis: not P is empty
consider a being Element of rng P;
ex b being set st [b,a] in P by RELAT_1:def 5;
hence not P is empty ; :: thesis: verum