let F be Graph-yielding Function; :: thesis:

hereby :: thesis:

assume A1: F is plain ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A2: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A3: ( F . x = G0 & G0 is plain ) by A1, A2, GLIBPRE0:def 1;
thus G is plain by A2, A3; :: thesis:

end;

hence rng F is plain ; :: thesis:

end;

hereby :: thesis:

assume A4: rng F is plain ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A5: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A5, FUNCT_1:3;
hence ( F . x = G & G is plain ) by A4; :: thesis:

end;

hence F is plain by GLIBPRE0:def 1; :: thesis:

end;

hereby :: thesis:

assume A6: F is loopless ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A7: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A8: ( F . x = G0 & G0 is loopless ) by A6, A7, GLIB_000:def 59;
thus G is loopless by A7, A8; :: thesis:

end;

hence rng F is loopless ; :: thesis:

end;

hereby :: thesis:

assume A9: rng F is loopless ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A10: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A10, FUNCT_1:3;
hence ( F . x = G & G is loopless ) by A9; :: thesis:

end;

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

end;

hereby :: thesis:

assume A11: F is non-multi ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A12: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A13: ( F . x = G0 & G0 is non-multi ) by A11, A12, GLIB_000:def 62;
thus G is non-multi by A12, A13; :: thesis:

end;

hence rng F is non-multi ; :: thesis:

end;

hereby :: thesis:

assume A14: rng F is non-multi ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A15: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A15, FUNCT_1:3;
hence ( F . x = G & G is non-multi ) by A14; :: thesis:

end;

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

end;

hereby :: thesis:

assume A16: F is non-Dmulti ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A17: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A18: ( F . x = G0 & G0 is non-Dmulti ) by A16, A17, GLIB_000:def 63;
thus G is non-Dmulti by A17, A18; :: thesis:

end;

hence rng F is non-Dmulti ; :: thesis:

end;

hereby :: thesis:

assume A19: rng F is non-Dmulti ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A20: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A20, FUNCT_1:3;
hence ( F . x = G & G is non-Dmulti ) by A19; :: thesis:

end;

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

end;

hereby :: thesis:

assume A21: F is acyclic ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A22: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A23: ( F . x = G0 & G0 is acyclic ) by A21, A22, GLIB_002:def 13;
thus G is acyclic by A22, A23; :: thesis:

end;

hence rng F is acyclic ; :: thesis:

end;

hereby :: thesis:

assume A24: rng F is acyclic ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A25: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A25, FUNCT_1:3;
hence ( F . x = G & G is acyclic ) by A24; :: thesis:

end;

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

end;

hereby :: thesis:

assume A26: F is connected ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A27: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A28: ( F . x = G0 & G0 is connected ) by A26, A27, GLIB_002:def 12;
thus G is connected by A27, A28; :: thesis:

end;

hence rng F is connected ; :: thesis:

end;

hereby :: thesis:

assume A29: rng F is connected ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A30: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A30, FUNCT_1:3;
hence ( F . x = G & G is connected ) by A29; :: thesis:

end;

hence F is connected by GLIB_002:def 12; :: thesis:

end;

hereby :: thesis:

assume A31: F is chordal ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A32: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A33: ( F . x = G0 & G0 is chordal ) by A31, A32, GLIBPRE0:def 4;
thus G is chordal by A32, A33; :: thesis:

end;

hence rng F is chordal ; :: thesis:

end;

hereby :: thesis:

assume A34: rng F is chordal ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A35: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A35, FUNCT_1:3;
hence ( F . x = G & G is chordal ) by A34; :: thesis:

end;

hence F is chordal by GLIBPRE0:def 4; :: thesis:

end;

hereby :: thesis:

assume A36: F is edgeless ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A37: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A38: ( F . x = G0 & G0 is edgeless ) by A36, A37, GLIB_008:def 2;
thus G is edgeless by A37, A38; :: thesis:

end;

hence rng F is edgeless ; :: thesis:

end;

hereby :: thesis:

assume A39: rng F is edgeless ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A40: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A40, FUNCT_1:3;
hence ( F . x = G & G is edgeless ) by A39; :: thesis:

end;

hence F is edgeless by GLIB_008:def 2; :: thesis:

end;

hereby :: thesis:

assume A41: F is loopfull ; :: thesis:

now :: thesis:

let G be _Graph; :: thesis:
assume G in rng F ; :: thesis:
then consider x being object such that
A42: ( x in dom F & F . x = G ) by FUNCT_1:def 3;
consider G0 being _Graph such that
A43: ( F . x = G0 & G0 is loopfull ) by A41, A42, GLIB_012:def 2;
thus G is loopfull by A42, A43; :: thesis:

end;

hence rng F is loopfull ; :: thesis:

end;

hereby :: thesis:

assume A44: rng F is loopfull ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A45: x in dom F ; :: thesis:
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G = G; :: thesis:
G in rng F by A45, FUNCT_1:3;
hence ( F . x = G & G is loopfull ) by A44; :: thesis:

end;

hence F is loopfull by GLIB_012:def 2; :: thesis:

end;