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

now :: thesis: for z being object st z in dom (~ f) holds
ex x, y being object st z = [x,y]

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

end;

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