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