A1: dom G c= NAT by Def1;
dom (G | X) c= dom G by RELAT_1:89;
then A2: dom (G | X) c= NAT by A1, XBOOLE_1:1;
G | X is finite by FINSET_1:13, RELAT_1:88;
hence G | X is GraphStruct by A2, Def1; :: thesis: verum