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