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 consider z being set such that
A3: ( [z,y] in W & z in {x} ) by RELAT_1:def 13;
thus [x,y] in W by A3, TARSKI:def 1; :: thesis: verum

end;

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

end;

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