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