let a, b, c, d, e, f be object ; rng {[a,b],[c,d],[e,f]} = {b,d,f}
A1:
rng {[a,b],[c,d]} = {b,d}
by RELAT_1:10;
A2:
rng {[e,f]} = {f}
by RELAT_1:9;
{[a,b],[c,d],[e,f]} = {[a,b],[c,d]} \/ {[e,f]}
by ENUMSET1:3;
hence rng {[a,b],[c,d],[e,f]} =
(rng {[a,b],[c,d]}) \/ (rng {[e,f]})
by XTUPLE_0:27
.=
{b,d,f}
by A1, A2, ENUMSET1:3
;
verum