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 set ; :: 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 consider x, y being set such that
A2: z = [y,x] and
A3: [x,y] in dom f by Def2;
thus z in [:Y,X:] by A1, A2, A3, ZFMISC_1:107; :: thesis: verum