now

let x be set ; :: thesis: ( x in union X implies ex y, z being set st x = [y,z] )
assume x in union X ; :: thesis: ex y, z being set st x = [y,z]
then consider Y being set such that
C0: ( x in Y & Y in X ) by TARSKI:def 4;
thus ex y, z being set st x = [y,z] by C0, RELAT_1:def 1; :: thesis: verum

end;

hence union X is Relation-like by RELAT_1:def 1; :: thesis: verum