let X, Y be set ; :: thesis: for R being Relation of X,Y holds
( dom (R ~) = rng R & rng (R ~) = dom R )
let R be Relation of X,Y; :: thesis: ( dom (R ~) = rng R & rng (R ~) = dom R )
now :: thesis: for x being object holds
( x in dom (R ~) iff x in rng R )
let x be object ; :: thesis: ( x in dom (R ~) iff x in rng R )
A1: now :: thesis: ( x in rng R implies x in dom (R ~) )
assume x in rng R ; :: thesis: x in dom (R ~)
then consider y being object such that
A2: [y,x] in R by XTUPLE_0:def 13;
[x,y] in R ~ by A2, RELAT_1:def 7;
hence x in dom (R ~) by XTUPLE_0:def 12; :: thesis: verum
end;
now :: thesis: ( x in dom (R ~) implies x in rng R )
assume x in dom (R ~) ; :: thesis: x in rng R
then consider y being object such that
A3: [x,y] in R ~ by XTUPLE_0:def 12;
[y,x] in R by A3, RELAT_1:def 7;
hence x in rng R by XTUPLE_0:def 13; :: thesis: verum
end;
hence ( x in dom (R ~) iff x in rng R ) by A1; :: thesis: verum
end;
hence dom (R ~) = rng R by TARSKI:2; :: thesis: rng (R ~) = dom R
now :: thesis: for x being object holds
( x in rng (R ~) iff x in dom R )
let x be object ; :: thesis: ( x in rng (R ~) iff x in dom R )
A4: now :: thesis: ( x in dom R implies x in rng (R ~) )
assume x in dom R ; :: thesis: x in rng (R ~)
then consider y being object such that
A5: [x,y] in R by XTUPLE_0:def 12;
[y,x] in R ~ by A5, RELAT_1:def 7;
hence x in rng (R ~) by XTUPLE_0:def 13; :: thesis: verum
end;
now :: thesis: ( x in rng (R ~) implies x in dom R )
assume x in rng (R ~) ; :: thesis: x in dom R
then consider y being object such that
A6: [y,x] in R ~ by XTUPLE_0:def 13;
[x,y] in R by A6, RELAT_1:def 7;
hence x in dom R by XTUPLE_0:def 12; :: thesis: verum
end;
hence ( x in rng (R ~) iff x in dom R ) by A4; :: thesis: verum
end;
hence rng (R ~) = dom R by TARSKI:2; :: thesis: verum