let G be loopless _Graph; :: thesis: ( G is edgeless iff SubtreeRel G = id (G .allTrees()) )

hereby :: thesis: ( SubtreeRel G = id (G .allTrees()) implies G is edgeless )

assume A1: G is edgeless ; :: thesis: SubtreeRel G = id (G .allTrees())

now :: thesis: for x, y being object holds
( ( [x,y] in SubtreeRel G implies ( x in G .allTrees() & x = y ) ) & ( x in G .allTrees() & x = y implies [x,y] in SubtreeRel G ) )

let x, y be object ; :: thesis: ( ( [x,y] in SubtreeRel G implies ( x in G .allTrees() & x = y ) ) & ( x in G .allTrees() & x = y implies [x,y] in SubtreeRel G ) )

hereby :: thesis: ( x in G .allTrees() & x = y implies [x,y] in SubtreeRel G )

assume A2: [x,y] in SubtreeRel G ; :: thesis: ( x in G .allTrees() & x = y )
then x in field (SubtreeRel G) by RELAT_1:15;
hence x in G .allTrees() by Th160; :: thesis: x = y
then reconsider T1 = x as Tree-like plain Subgraph of G by Th138;
y in field (SubtreeRel G) by A2, RELAT_1:15;
then y in G .allTrees() by Th160;
then reconsider T2 = y as Tree-like plain Subgraph of G by Th138;
A3: T2 is edgeless by A1;
then consider v being Vertex of T2 such that
A4: the_Vertices_of T2 = {v} by GLIB_000:22;
A5: T1 is Subgraph of T2 by A2, Th159;
then the_Vertices_of T1 c= the_Vertices_of T2 by GLIB_000:def 32;
then A6: the_Vertices_of T2 c= the_Vertices_of T1 by A4, ZFMISC_1:33;
the_Edges_of T2 = {} by A3;
then the_Edges_of T2 c= the_Edges_of T1 by XBOOLE_1:2;
then T2 is Subgraph of T1 by A6, GLIB_000:44;
hence x = y by A5, GLIB_000:87, GLIB_009:44; :: thesis: verum

end;

assume A7: ( x in G .allTrees() & x = y ) ; :: thesis: [x,y] in SubtreeRel G
SubtreeRel G is_reflexive_in field (SubtreeRel G) by RELAT_2:def 9;
then SubtreeRel G is_reflexive_in G .allTrees() by Th160;
hence [x,y] in SubtreeRel G by A7, RELAT_2:def 1; :: thesis: verum

end;

hence SubtreeRel G = id (G .allTrees()) by RELAT_1:def 10; :: thesis: verum

end;

assume A8: SubtreeRel G = id (G .allTrees()) ; :: thesis: G is edgeless
assume not G is edgeless ; :: thesis: contradiction
then reconsider G9 = G as non edgeless _Graph ;
set e = the Edge of G9;
set v = (the_Source_of G9) . the Edge of G9;
set w = (the_Target_of G9) . the Edge of G9;
set V = {((the_Source_of G9) . the Edge of G9),((the_Target_of G9) . the Edge of G9)};
A9: the Edge of G9 Joins (the_Source_of G9) . the Edge of G9,(the_Target_of G9) . the Edge of G9,G9 by GLIB_000:def 13;
reconsider V = {((the_Source_of G9) . the Edge of G9),((the_Target_of G9) . the Edge of G9)} as non empty Subset of (the_Vertices_of G9) ;
set S = the Edge of G9 .--> ((the_Source_of G9) . the Edge of G9);
set T = the Edge of G9 .--> ((the_Target_of G9) . the Edge of G9);
( dom ( the Edge of G9 .--> ((the_Source_of G9) . the Edge of G9)) = dom {[ the Edge of G9,((the_Source_of G9) . the Edge of G9)]} & dom ( the Edge of G9 .--> ((the_Target_of G9) . the Edge of G9)) = dom {[ the Edge of G9,((the_Target_of G9) . the Edge of G9)]} ) by FUNCT_4:82;
then A10: ( dom ( the Edge of G9 .--> ((the_Source_of G9) . the Edge of G9)) = { the Edge of G9} & dom ( the Edge of G9 .--> ((the_Target_of G9) . the Edge of G9)) = { the Edge of G9} ) by RELAT_1:9;
( rng ( the Edge of G9 .--> ((the_Source_of G9) . the Edge of G9)) = {((the_Source_of G9) . the Edge of G9)} & rng ( the Edge of G9 .--> ((the_Target_of G9) . the Edge of G9)) = {((the_Target_of G9) . the Edge of G9)} ) by FUNCOP_1:88;
then reconsider S = the Edge of G9 .--> ((the_Source_of G9) . the Edge of G9), T = the Edge of G9 .--> ((the_Target_of G9) . the Edge of G9) as Function of { the Edge of G9},V by A10, FUNCT_2:2, ZFMISC_1:7;
set H9 = createGraph the Edge of G9;
not the Edge of G9 in G9 .loops() ;
then A11: createGraph the Edge of G9 in G .allTrees() by Th143;
set H8 = the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)};
the_Edges_of (createGraph the Edge of G9) = { the Edge of G9} by Th13;
then A12: the Edge of G9 in the_Edges_of (createGraph the Edge of G9) by TARSKI:def 1;
the Edge of G9 Joins (the_Source_of G9) . the Edge of G9,(the_Target_of G9) . the Edge of G9, createGraph the Edge of G9 by A12, A9, GLIB_000:73;
then A14: (the_Source_of G9) . the Edge of G9 is Vertex of (createGraph the Edge of G9) by GLIB_000:13;
A15: the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is Subgraph of G by GLIB_000:43;
( the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is loopless & the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is _trivial ) by A14;
then A16: ( the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is _trivial & the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is edgeless ) ;
then A17: the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} is Tree-like plain Subgraph of G by A15;
A18: the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)} <> createGraph the Edge of G9 by A16;
[ the plain inducedSubgraph of (createGraph the Edge of G9),{((the_Source_of G9) . the Edge of G9)},(createGraph the Edge of G9)] in SubtreeRel G by A11, A17, Th159;
hence contradiction by A18, A8, RELAT_1:def 10; :: thesis: verum