rng <%x%> c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <%x%> or y in D )
assume y in rng <%x%> ; :: thesis: y in D
then y in {x} by Th36;
then y = x by TARSKI:def 1;
hence y in D ; :: thesis: verum

end;

hence <%x%> is XFinSequence of D by RELAT_1:def 19; :: thesis: verum