let G be Tree-like _Graph; for H being spanning Subgraph of G st H is connected holds
G == H
let H be spanning Subgraph of G; ( H is connected implies G == H )
assume A1:
H is connected
; G == H
A2:
G is Subgraph of G
by GLIB_000:40;
A3:
the_Vertices_of G = the_Vertices_of H
by GLIB_000:def 33;
the_Edges_of G c= the_Edges_of H
proof
assume
not
the_Edges_of G c= the_Edges_of H
;
contradiction
then
(the_Edges_of G) \ (the_Edges_of H) <> {}
by XBOOLE_1:37;
then consider e being
object such that A4:
e in (the_Edges_of G) \ (the_Edges_of H)
by XBOOLE_0:def 1;
set v =
(the_Source_of G) . e;
set w =
(the_Target_of G) . e;
A5:
(
e in the_Edges_of G & not
e in the_Edges_of H )
by A4, XBOOLE_0:def 5;
then A6:
e Joins (the_Source_of G) . e,
(the_Target_of G) . e,
G
by GLIB_000:def 13;
then reconsider v =
(the_Source_of G) . e,
w =
(the_Target_of G) . e as
Vertex of
G by GLIB_000:13;
reconsider v1 =
v,
w1 =
w as
Vertex of
H by A3;
consider W9 being
Walk of
H such that A7:
W9 is_Walk_from v1,
w1
by A1, GLIB_002:def 1;
set P9 = the
Path of
W9;
reconsider P = the
Path of
W9 as
Path of
G by GLIB_001:167, GLIB_001:176;
the
Path of
W9 is_Walk_from v1,
w1
by A7, GLIB_001:160;
then A8:
P is_Walk_from v,
w
by GLIB_001:19;
G .walkOf (
v,
e,
w) =
G .pathBetween (
v,
w)
by A6, GLIB_008:29
.=
the
Path of
W9
by A8, HELLY:def 2
;
then the
Path of
W9 .edges() =
(G .walkOf (v,e,w)) .edges()
by GLIB_001:110
.=
{e}
by A6, GLIB_001:108
;
then
e in the
Path of
W9 .edges()
by TARSKI:def 1;
hence
contradiction
by A5;
verum
end;
then
G is Subgraph of H
by A2, A3, GLIB_000:44;
hence
G == H
by GLIB_000:87; verum