let Y, X be set ; :: thesis: for R being Relation of X,Y st id X c= R holds
( X = dom R & X c= rng R )
let R be Relation of X,Y; :: thesis: ( id X c= R implies ( X = dom R & X c= rng R ) )
assume A1: id X c= R ; :: thesis: ( X = dom R & X c= rng R )
then X c= dom R by Th30;
hence X = dom R by XBOOLE_0:def 10; :: thesis: X c= rng R
thus X c= rng R by A1, Th30; :: thesis: verum