A1: field (SubtreeRel G) = G .allTrees() by Th160;
SubtreeRel G partially_orders G .allTrees() by Th161;
then consider x being set such that
A2: x is_maximal_in SubtreeRel G by A1, Th166, ORDERS_1:63;
x in field (SubtreeRel G) by A2, ORDERS_1:def 12;
then reconsider T = x as Tree-like plain Subgraph of G by A1, Th138;
take T ; :: thesis: ( T is plain & T is spanning & T is Tree-like )

per cases ( G is _trivial or not G is _trivial ) ;

suppose G is _trivial ; :: thesis: ( T is plain & T is spanning & T is Tree-like )

hence ( T is plain & T is spanning & T is Tree-like ) by GLIB_000:121; :: thesis: verum

end;

suppose A3: not G is _trivial ; :: thesis: ( T is plain & T is spanning & T is Tree-like )

now :: thesis: T is spanning

assume not T is spanning ; :: thesis: contradiction
then consider v, e, w being object such that
A4: ( v <> w & e DJoins v,w,G & not e in the_Edges_of T ) and
A5: for G3 being addAdjVertex of T,v,e,w holds G3 is Subgraph of G and
A6: ( ( v in the_Vertices_of T & not w in the_Vertices_of T ) or ( not v in the_Vertices_of T & w in the_Vertices_of T ) ) by A3, GLIBPRE1:61;
set G3 = the plain addAdjVertex of T,v,e,w;
reconsider G3 = the plain addAdjVertex of T,v,e,w as Tree-like plain Subgraph of G by A5;
e DJoins v,w,G3 by A4, A6, GLIB_006:131, GLIB_006:132;
then A7: T <> G3 by A4, GLIB_000:def 14;
A8: G3 in field (SubtreeRel G) by A1, Th138;
T is Subgraph of G3 by GLIB_006:57;
then [T,G3] in SubtreeRel G by Th159;
hence contradiction by A2, A7, A8, ORDERS_1:def 12; :: thesis: verum

end;

hence ( T is plain & T is spanning & T is Tree-like ) ; :: thesis: verum

end;

end;