let x be Element of dom <*G*>; :: according to GLIB_008:def 3 :: thesis: <*G*> . x is edgeless
x in dom <*G*> ;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*G*> . x is edgeless ; :: thesis: verum