let X, Y be set ; :: thesis: rng [:X,Y:] c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng [:X,Y:] or x in Y )
assume x in rng [:X,Y:] ; :: thesis: x in Y
then ex y being set st [y,x] in [:X,Y:] by Def5;
hence x in Y by ZFMISC_1:87; :: thesis: verum