let Y be set ; :: thesis: for R being Y -defined total Relation holds id Y c= R * (R ~)
set X = Y;
let R be Y -defined total Relation; :: thesis: id Y c= R * (R ~)
reconsider f = id Y as Function ;
B0: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20;

now

let z be set ; :: thesis: ( z in f implies z in R * (R ~) )
assume z in f ; :: thesis: z in R * (R ~)
then consider x being Element of dom f such that
C2: ( z = [x,((id Y) . x)] & x in dom (id Y) ) by B0;
C0: ( x in Y & z = [x,x] ) by C2, FUNCT_1:17;
x in dom R by C0, PARTFUN1:def 2;
then consider y being set such that
C1: [x,y] in R by RELAT_1:def 4;
[y,x] in R ~ by C1, RELAT_1:def 7;
then [x,x] in R * (R ~) by C1, RELAT_1:def 8;
hence z in R * (R ~) by C2, FUNCT_1:17; :: thesis: verum

end;

hence id Y c= R * (R ~) by TARSKI:def 3; :: thesis: verum