let X, Y be set ; :: thesis: dom [:X,Y:] c= X
let x be set ; :: 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 set st [x,y] in [:X,Y:] by Def4;
hence x in X by ZFMISC_1:87; :: thesis: verum