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

let x, y be set ; :: 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, Th39;
then y in Im W,x by Def5;
then ex z being set 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 RELAT_1:def 4;
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, Th39; :: thesis: verum

end;

hence *graph (W,X *graph ) = W by RELAT_1:def 2; :: thesis: verum