now :: thesis: for x being object st x in union X holds
ex y, z being object st x = [y,z]

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

end;

hence for b₁ being set st b₁ = union X holds
b₁ is Relation-like ; :: thesis: verum