let A, X, Y be set ; :: thesis: for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )
let R be Relation of X,Y; :: thesis: ( id A c= R implies ( A c= dom R & A c= rng R ) )
assume A1: id A c= R ; :: thesis: ( A c= dom R & A c= rng R )
thus A c= dom R :: thesis: A c= rng R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in dom R )
assume x in A ; :: thesis: x in dom R
then [x,x] in id A by RELAT_1:def 10;
hence x in dom R by A1, XTUPLE_0:def 12; :: thesis: verum

end;

thus A c= rng R :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng R )
assume x in A ; :: thesis: x in rng R
then [x,x] in id A by RELAT_1:def 10;
hence x in rng R by A1, XTUPLE_0:def 13; :: thesis: verum

end;