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;

*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) ) )

hence
*graph ((W,X) *graph) = W
; :: thesis: verum( ( [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) ) )

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;hereby :: thesis: ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) )

assume A3:
[x,y] in W
; :: thesis: [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;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

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