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 ;
A1: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20;

now :: thesis: for z being object st z in f holds
z in R * (R ~)

let z be object ; :: 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
A2: ( z = [x,((id Y) . x)] & x in dom (id Y) ) by A1;
x in dom R by A2, PARTFUN1:def 2;
then consider y being object such that
A3: [x,y] in R by XTUPLE_0:def 12;
[y,x] in R ~ by A3, RELAT_1:def 7;
then [x,x] in R * (R ~) by A3, RELAT_1:def 8;
hence z in R * (R ~) by A2; :: thesis: verum

end;

hence id Y c= R * (R ~) ; :: thesis: verum