let S1, S2 be Graph-membered set ; :: thesis:
assume S1,S2 are_isomorphic ; :: thesis:
then consider f being one-to-one Function such that
A1: ( dom f = S1 & rng f = S2 ) and
A2: for G being _Graph st G in S1 holds
f . G is b₁ -isomorphic _Graph ;

hereby :: thesis:

assume S1 is empty ; :: thesis:
then f = {} by A1;
hence S2 is empty by A1; :: thesis:

end;

hereby :: thesis:

assume A3: S1 is loopless ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A4: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A4;
G2 is G1 -isomorphic by A1, A2, A4;
then consider G being PGraphMapping of G1,G2 such that
A5: G is isomorphism by GLIB_010:def 23;
thus G2 is loopless by A1, A3, A4, A5, GLIB_010:89; :: thesis:

end;

hence S2 is loopless by GLIB_014:def 3; :: thesis:

end;

hereby :: thesis:

assume A6: S1 is non-multi ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A7: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A7;
G2 is G1 -isomorphic by A1, A2, A7;
then consider G being PGraphMapping of G1,G2 such that
A8: G is isomorphism by GLIB_010:def 23;
thus G2 is non-multi by A1, A6, A7, A8, GLIB_010:89; :: thesis:

end;

hence S2 is non-multi by GLIB_014:def 4; :: thesis:

end;

hereby :: thesis:

assume A9: S1 is simple ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A10: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A10;
G2 is G1 -isomorphic by A1, A2, A10;
then consider G being PGraphMapping of G1,G2 such that
A11: G is isomorphism by GLIB_010:def 23;
thus G2 is simple by A1, A9, A10, A11, GLIB_010:89; :: thesis:

end;

hence S2 is simple by GLIB_014:def 6; :: thesis:

end;

hereby :: thesis:

assume A12: S1 is acyclic ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A13: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A13;
G2 is G1 -isomorphic by A1, A2, A13;
then consider G being PGraphMapping of G1,G2 such that
A14: G is isomorphism by GLIB_010:def 23;
thus G2 is acyclic by A1, A12, A13, A14, GLIB_010:140; :: thesis:

end;

hence S2 is acyclic by GLIB_014:def 8; :: thesis:

end;

hereby :: thesis:

assume A15: S1 is connected ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A16: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A16;
G2 is G1 -isomorphic by A1, A2, A16;
then consider G being PGraphMapping of G1,G2 such that
A17: G is isomorphism by GLIB_010:def 23;
thus G2 is connected by A1, A15, A16, A17, GLIB_010:140; :: thesis:

end;

hence S2 is connected by GLIB_014:def 9; :: thesis:

end;

hereby :: thesis:

assume A18: S1 is Tree-like ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A19: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A19;
G2 is G1 -isomorphic by A1, A2, A19;
then consider G being PGraphMapping of G1,G2 such that
A20: G is isomorphism by GLIB_010:def 23;
( G2 is connected & G2 is acyclic ) by A1, A18, A19, A20, GLIB_010:140;
hence G2 is Tree-like ; :: thesis:

end;

hence S2 is Tree-like by GLIB_014:def 10; :: thesis:

end;

hereby :: thesis:

assume A21: S1 is chordal ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A22: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A22;
G2 is G1 -isomorphic by A1, A2, A22;
then consider G being PGraphMapping of G1,G2 such that
A23: G is isomorphism by GLIB_010:def 23;
thus G2 is chordal by A1, A21, A22, A23, GLIB_010:140; :: thesis:

end;

hence S2 is chordal by GLIB_014:def 11; :: thesis:

end;

hereby :: thesis:

assume A24: S1 is edgeless ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A25: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A25;
G2 is G1 -isomorphic by A1, A2, A25;
then consider G being PGraphMapping of G1,G2 such that
A26: G is isomorphism by GLIB_010:def 23;
thus G2 is edgeless by A1, A24, A25, A26, GLIB_010:89; :: thesis:

end;

hence S2 is edgeless by GLIB_014:def 12; :: thesis:

end;

hereby :: thesis:

assume A27: S1 is loopfull ; :: thesis:

now :: thesis:

let G2 be _Graph; :: thesis:
assume G2 in S2 ; :: thesis:
then consider G1 being object such that
A28: ( G1 in dom f & f . G1 = G2 ) by A1, FUNCT_1:def 3;
reconsider G1 = G1 as _Graph by A1, A28;
G2 is G1 -isomorphic by A1, A2, A28;
then consider G being PGraphMapping of G1,G2 such that
A29: G is isomorphism by GLIB_010:def 23;
thus G2 is loopfull by A1, A27, A28, A29, GLIB_012:10; :: thesis:

end;

hence S2 is loopfull by GLIB_014:def 13; :: thesis:

end;