let W be Relation; :: thesis: for X being set st dom W c= X holds
*graph ((W,X) *graph) = W
let X be set ; :: thesis: ( dom W c= X implies *graph ((W,X) *graph) = W )
assume A1: dom W c= X ; :: thesis: *graph ((W,X) *graph) = W
A2: dom ((W,X) *graph) = X by Def5;

now :: thesis: for x, y being object holds
( ( [x,y] in *graph ((W,X) *graph) implies [x,y] in W ) & ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) ) )

let x, y be object ; :: thesis: ( ( [x,y] in *graph ((W,X) *graph) implies [x,y] in W ) & ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) ) )

hereby :: thesis: ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) )

assume [x,y] in *graph ((W,X) *graph) ; :: thesis: [x,y] in W
then ( x in X & y in ((W,X) *graph) . x ) by A2, Th38;
then y in Im (W,x) by Def5;
then ex z being object st
( [z,y] in W & z in {x} ) by RELAT_1:def 13;
hence [x,y] in W by TARSKI:def 1; :: thesis: verum

end;

assume A3: [x,y] in W ; :: thesis: [x,y] in *graph ((W,X) *graph)
then A4: x in dom W by XTUPLE_0:def 12;
x in {x} by TARSKI:def 1;
then y in Im (W,x) by A3, RELAT_1:def 13;
then y in ((W,X) *graph) . x by A1, A4, Def5;
hence [x,y] in *graph ((W,X) *graph) by A1, A2, A4, Th38; :: thesis: verum

end;

hence *graph ((W,X) *graph) = W ; :: thesis: verum