let G be _Graph; :: thesis: for S being non empty Subset of (G .allSG())
for G9 being GraphUnion of S st (SubgraphRel G) |_2 S is being_linear-order holds
for W being Walk of G9 ex H being Element of S st W is Walk of H
let S be non empty Subset of (G .allSG()); :: thesis: for G9 being GraphUnion of S st (SubgraphRel G) |_2 S is being_linear-order holds
for W being Walk of G9 ex H being Element of S st W is Walk of H
let G9 be GraphUnion of S; :: thesis: ( (SubgraphRel G) |_2 S is being_linear-order implies for W being Walk of G9 ex H being Element of S st W is Walk of H )
set R = (SubgraphRel G) |_2 S;
assume A1: (SubgraphRel G) |_2 S is being_linear-order ; :: thesis: for W being Walk of G9 ex H being Element of S st W is Walk of H
defpred S₁[ Walk of G9] means ex H being Element of S st $1 is Walk of H;
A2: for W being trivial Walk of G9 holds S₁[W]

proof

let W be trivial Walk of G9; :: thesis: S₁[W]
consider v9 being Vertex of G9 such that
A3: W = G9 .walkOf v9 by GLIB_001:128;
the_Vertices_of G9 = union (the_Vertices_of S) by GLIB_014:def 25;
then consider V being set such that
A4: ( v9 in V & V in the_Vertices_of S ) by TARSKI:def 4;
consider H being _Graph such that
A5: ( H in S & V = the_Vertices_of H ) by A4, GLIB_014:def 14;
reconsider H = H as Element of S by A5;
take H ; :: thesis: W is Walk of H
reconsider v = v9 as Vertex of H by A4, A5;
W = <*v*> by A3, GLIB_001:def 4
.= H .walkOf v by GLIB_001:def 4 ;
hence W is Walk of H ; :: thesis: verum

end;

A6: for W being Walk of G9
for e being object st e in (W .last()) .edgesInOut() & S₁[W] holds
S₁[W .addEdge e]

proof

let W be Walk of G9; :: thesis: for e being object st e in (W .last()) .edgesInOut() & S₁[W] holds
S₁[W .addEdge e]
let e be object ; :: thesis: ( e in (W .last()) .edgesInOut() & S₁[W] implies S₁[W .addEdge e] )
assume A7: ( e in (W .last()) .edgesInOut() & S₁[W] ) ; :: thesis: S₁[W .addEdge e]
then e in the_Edges_of G9 ;
then e in union (the_Edges_of S) by GLIB_014:def 25;
then consider E being set such that
A8: ( e in E & E in the_Edges_of S ) by TARSKI:def 4;
consider H2 being _Graph such that
A9: ( H2 in S & E = the_Edges_of H2 ) by A8, GLIB_014:def 15;
reconsider H2 = H2 as Element of S by A9;
consider H1 being Element of S such that
A10: W is Walk of H1 by A7;
( (SubgraphRel G) |_2 S is reflexive & (SubgraphRel G) |_2 S is connected ) by A1, ORDERS_1:def 6;
then A11: (SubgraphRel G) |_2 S is_strongly_connected_in field ((SubgraphRel G) |_2 S) by RELAT_2:def 15;
A12: field (SubgraphRel G) = G .allSG() by Th40;
then field ((SubgraphRel G) |_2 S) = S by ORDERS_1:71;
then A13: ( H1 in field ((SubgraphRel G) |_2 S) & H2 in field ((SubgraphRel G) |_2 S) ) ;
then A14: ( H1 in G .allSG() & H2 in G .allSG() ) by A12, WELLORD1:12;
consider w being Vertex of G9 such that
A15: e Joins W .last() ,w,G9 by A7, GLIB_000:64;
A16: ( H1 is Subgraph of G9 & H2 is Subgraph of G9 ) by GLIB_014:21;
then A17: e Joins W .last() ,w,H2 by A8, A9, A15, GLIB_000:73;

per cases ( [H1,H2] in (SubgraphRel G) |_2 S or [H2,H1] in (SubgraphRel G) |_2 S ) by A11, A13, RELAT_2:def 7;

suppose [H1,H2] in (SubgraphRel G) |_2 S ; :: thesis: S₁[W .addEdge e]

then [H1,H2] in SubgraphRel G by MMLQUER2:4;
then H1 is Subgraph of H2 by A14, Def6;
then reconsider W2 = W as Walk of H2 by A10, GLIB_001:167;
take H2 ; :: thesis: W .addEdge e is Walk of H2
W .last() = W2 .last() by GLIB_001:16;
then e in (W2 .last()) .edgesInOut() by A17, GLIB_000:62;
then W .addEdge e = W2 .addEdge e by A16, GLIB_001:174;
hence W .addEdge e is Walk of H2 ; :: thesis: verum

end;

suppose [H2,H1] in (SubgraphRel G) |_2 S ; :: thesis: S₁[W .addEdge e]

then [H2,H1] in SubgraphRel G by MMLQUER2:4;
then H2 is Subgraph of H1 by A14, Def6;
then A18: e Joins W .last() ,w,H1 by A17, GLIB_000:72;
reconsider W1 = W as Walk of H1 by A10;
take H1 ; :: thesis: W .addEdge e is Walk of H1
W .last() = W1 .last() by GLIB_001:16;
then e in (W1 .last()) .edgesInOut() by A18, GLIB_000:62;
then W .addEdge e = W1 .addEdge e by A16, GLIB_001:174;
hence W .addEdge e is Walk of H1 ; :: thesis: verum

end;

end;

end;

for W being Walk of G9 holds S₁[W] from GLIB_009:sch 1(A2, A6);
hence for W being Walk of G9 ex H being Element of S st W is Walk of H ; :: thesis: verum