let x be object ; :: according to GLIB_000:def 53 :: thesis: ( not x in dom <*G*> or <*G*> . x is set )
assume x in dom <*G*> ; :: thesis: <*G*> . x is set
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*G*> . x is _Graph by FINSEQ_1:def 8; :: thesis: verum