let f be Function; :: thesis: ex X, Y being set st dom (~ f) c= [:X,Y:]

now

let z be set ; :: thesis: ( z in dom (~ f) implies ex x, y being set st z = [x,y] )
assume z in dom (~ f) ; :: thesis: ex x, y being set st z = [x,y]
then ex x, y being set st
( z = [y,x] & [x,y] in dom f ) by Def2;
hence ex x, y being set st z = [x,y] ; :: thesis: verum

end;

hence ex X, Y being set st dom (~ f) c= [:X,Y:] by Th1; :: thesis: verum