let R be Relation; :: thesis: ( rng R = dom (R ~) & dom R = rng (R ~) )
thus rng R c= dom (R ~) :: according to XBOOLE_0:def 10 :: thesis: ( dom (R ~) c= rng R & dom R = rng (R ~) )
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng R or u in dom (R ~) )
assume u in rng R ; :: thesis: u in dom (R ~)
then consider x being object such that
A1: [x,u] in R by XTUPLE_0:def 13;
[u,x] in R ~ by A1, Def5;
hence u in dom (R ~) by XTUPLE_0:def 12; :: thesis: verum
end;
thus dom (R ~) c= rng R :: thesis: dom R = rng (R ~)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in dom (R ~) or u in rng R )
assume u in dom (R ~) ; :: thesis: u in rng R
then consider x being object such that
A2: [u,x] in R ~ by XTUPLE_0:def 12;
[x,u] in R by A2, Def5;
hence u in rng R by XTUPLE_0:def 13; :: thesis: verum
end;
thus dom R c= rng (R ~) :: according to XBOOLE_0:def 10 :: thesis: rng (R ~) c= dom R
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in dom R or u in rng (R ~) )
assume u in dom R ; :: thesis: u in rng (R ~)
then consider x being object such that
A3: [u,x] in R by XTUPLE_0:def 12;
[x,u] in R ~ by A3, Def5;
hence u in rng (R ~) by XTUPLE_0:def 13; :: thesis: verum
end;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng (R ~) or u in dom R )
assume u in rng (R ~) ; :: thesis: u in dom R
then consider x being object such that
A4: [x,u] in R ~ by XTUPLE_0:def 13;
[u,x] in R by A4, Def5;
hence u in dom R by XTUPLE_0:def 12; :: thesis: verum