let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
dom (~ f) c= [:Y,X:]
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies dom (~ f) c= [:Y,X:] )
assume A1: dom f c= [:X,Y:] ; :: thesis: dom (~ f) c= [:Y,X:]
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom (~ f) or z in [:Y,X:] )
assume z in dom (~ f) ; :: thesis: z in [:Y,X:]
then ex x, y being object st
( z = [y,x] & [x,y] in dom f ) by Def2;
hence z in [:Y,X:] by A1, ZFMISC_1:88; :: thesis: verum