let GF be Graph-yielding Function; :: thesis:
assume A5: GF is edgeless ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A6: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A6; :: thesis:
thus G is non-multi by A6; :: thesis:

end;

hence GF is non-multi by GLIB_000:def 62; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A7: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A7; :: thesis:
thus G is non-Dmulti by A7; :: thesis:

end;

hence GF is non-Dmulti by GLIB_000:def 63; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A8: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A8; :: thesis:
thus G is loopless by A8; :: thesis:

end;

hence GF is loopless by GLIB_000:def 59; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A9: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A9; :: thesis:
thus G is simple by A9; :: thesis:

end;

hence GF is simple by GLIB_000:def 64; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A10: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A10; :: thesis:
thus G is Dsimple by A10; :: thesis:

end;

hence GF is Dsimple by GLIB_000:def 65; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in dom GF ; :: thesis:
then consider G being _Graph such that
A11: ( GF . x = G & G is edgeless ) by A5;
take G = G; :: thesis:
thus GF . x = G by A11; :: thesis:
thus G is acyclic by A11; :: thesis:

end;

hence GF is acyclic by GLIB_002:def 13; :: thesis: