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 b1 being set st b1 = union X holds
b1 is Relation-like ; :: thesis: verum