let G be _Graph; :: thesis:

let Y be set ; :: thesis:
assume that
A1: Y c= G .allTrees() and
A2: (SubtreeRel G) |_2 Y is being_linear-order ; :: thesis:

suppose A3: Y <> {} ; :: thesis:

A4: Y c= G .allSG() by A1, XBOOLE_1:1;
then reconsider S = Y as GraphUnionSet by A3;
set T = the plain GraphUnion of S;

let v1, v2 be Vertex of the plain GraphUnion of S; :: thesis:
A5: the_Vertices_of the plain GraphUnion of S = union (the_Vertices_of S) by GLIB_014:def 25;
then consider V1 being set such that
A6: ( v1 in V1 & V1 in the_Vertices_of S ) by TARSKI:def 4;
consider H1 being _Graph such that
A7: ( H1 in S & V1 = the_Vertices_of H1 ) by A6, GLIB_014:def 14;
consider V2 being set such that
A8: ( v2 in V2 & V2 in the_Vertices_of S ) by A5, TARSKI:def 4;
consider H2 being _Graph such that
A9: ( H2 in S & V2 = the_Vertices_of H2 ) by A8, GLIB_014:def 14;
reconsider H1 = H1, H2 = H2 as Element of G .allTrees() by A1, A7, A9;
Y c= field (SubtreeRel G) by A1, Th160;
then A10: field ((SubtreeRel G) |_2 Y) = Y by ORDERS_1:71;
( (SubtreeRel G) |_2 Y is reflexive & (SubtreeRel G) |_2 Y is connected ) by A2, ORDERS_1:def 6;

per cases in (SubtreeRel G) |_2 Y or [H2,H1] in (SubtreeRel G) |_2 Y ) by A7, A9, A10, RELAT_2:def 7, RELAT_2:def 15;

suppose [H1,H2] in (SubtreeRel G) |_2 Y ; :: thesis:

then [H1,H2] in SubtreeRel G by MMLQUER2:4;
then H1 is Subgraph of H2 by Th159;
then the_Vertices_of H1 c= the_Vertices_of H2 by GLIB_000:def 32;
then consider W2 being Walk of H2 such that
A11: W2 is_Walk_from v1,v2 by A6, A7, A8, A9, GLIB_002:def 1;
H2 is Subgraph of the plain GraphUnion of S by A9, GLIB_014:21;
then reconsider W = W2 as Walk of the plain GraphUnion of S by GLIB_001:167;
take W = W; :: thesis:
thus W is_Walk_from v1,v2 by A11, GLIB_001:19; :: thesis:

end;

suppose [H2,H1] in (SubtreeRel G) |_2 Y ; :: thesis:

then [H2,H1] in SubtreeRel G by MMLQUER2:4;
then H2 is Subgraph of H1 by Th159;
then the_Vertices_of H2 c= the_Vertices_of H1 by GLIB_000:def 32;
then consider W1 being Walk of H1 such that
A12: W1 is_Walk_from v1,v2 by A6, A7, A8, A9, GLIB_002:def 1;
H1 is Subgraph of the plain GraphUnion of S by A7, GLIB_014:21;
then reconsider W = W1 as Walk of the plain GraphUnion of S by GLIB_001:167;
take W = W; :: thesis:
thus W is_Walk_from v1,v2 by A12, GLIB_001:19; :: thesis:

end;

end;

end;

then reconsider T = the plain GraphUnion of S as connected _Graph by GLIB_002:def 1;

given W being Walk of T such that A13: W is Cycle-like ; :: thesis:
(SubtreeRel G) |_2 Y = (SubgraphRel G) |_2 S by A1, WELLORD1:22;
then consider H being Element of S such that
A14: W is Walk of H by A2, A4, Th44;
reconsider W = W as Walk of H by A14;
W is Cycle-like by A13, GLIB_006:24;
hence contradiction by A1, GLIB_002:def 2; :: thesis:

end;

then T is acyclic by GLIB_002:def 2;
then reconsider T = T as Tree-like _Graph ;
A15: S c= G .allSG() by A1, XBOOLE_1:1;
G is GraphUnion of G .allSG() by Th35;
then reconsider T = T as Tree-like Subgraph of G by A15, GLIBPRE1:119;
reconsider x = T as set ;
take x = x; :: thesis:
thus x in G .allTrees() by Th138; :: thesis:
let y be set ; :: thesis:
assume A16: y in Y ; :: thesis:
then reconsider T9 = y as Element of G .allTrees() by A1;
T9 is Subgraph of T by A16, GLIB_014:21;
hence [y,x] in SubtreeRel G by Th159; :: thesis:

end;

suppose A17: Y = {} ; :: thesis:

reconsider x = the Element of G .allTrees() as set ;
take x = x; :: thesis:
thus x in G .allTrees() ; :: thesis:
thus for y being set st y in Y holds
[y,x] in SubtreeRel G by A17; :: thesis:

end;

end;

end;

hence G .allTrees() has_upper_Zorn_property_wrt SubtreeRel G by ORDERS_1:def 10; :: thesis: