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