let X be set ; :: thesis: rng (delta X) c= [:X,X:]
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (delta X) or y in [:X,X:] )
assume y in rng (delta X) ; :: thesis: y in [:X,X:]
then consider x being set such that
A1: x in dom (delta X) and
A2: y = (delta X) . x by FUNCT_1:def 5;

now

thus x in X by A1, Def7; :: thesis: y = [x,x]
hence y = [x,x] by A2, Def7; :: thesis: verum

end;

hence y in [:X,X:] by ZFMISC_1:106; :: thesis: verum