for x being set st x in Union (disjoin f) holds
ex y, z being set st x = [y,z] by CARD_3:32;
hence Union (disjoin f) is Relation-like by RELAT_1:def 1; :: thesis: verum