let y be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not y in rng <*x*> or y in D )
assume y in rng <*x*> ; :: thesis: y in D
then y in {x} by Th39;
then y = x by TARSKI:def 1;
hence y in D ; :: thesis: verum