set V = {0 ,1};
set E = {0 };
set S = 0 .--> 0 ;
set T = 0 .--> 1;
A1: dom (0 .--> 1) = {0 } by FUNCOP_1:19;

A2: now

let x be set ; :: thesis: ( x in {0 } implies (0 .--> 1) . x in {0 ,1} )
assume x in {0 } ; :: thesis: (0 .--> 1) . x in {0 ,1}
then x = 0 by TARSKI:def 1;
then (0 .--> 1) . x = 1 by FUNCOP_1:87;
hence (0 .--> 1) . x in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

A3: now

let x be set ; :: thesis: ( x in {0 } implies (0 .--> 0 ) . x in {0 ,1} )
assume x in {0 } ; :: thesis: (0 .--> 0 ) . x in {0 ,1}
then x = 0 by TARSKI:def 1;
then (0 .--> 0 ) . x = 0 by FUNCOP_1:87;
hence (0 .--> 0 ) . x in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

reconsider T = 0 .--> 1 as Function of {0 },{0 ,1} by A1, A2, FUNCT_2:5;
dom (0 .--> 0 ) = {0 } by FUNCOP_1:19;
then reconsider S = 0 .--> 0 as Function of {0 },{0 ,1} by A3, FUNCT_2:5;
set G = createGraph {0 ,1},{0 },S,T;
A4: the_Edges_of (createGraph {0 ,1},{0 },S,T) = {0 } by GLIB_000:8;
the_Target_of (createGraph {0 ,1},{0 },S,T) = T by GLIB_000:8;
then A5: (the_Target_of (createGraph {0 ,1},{0 },S,T)) . 0 = 1 by FUNCOP_1:87;
the_Source_of (createGraph {0 ,1},{0 },S,T) = S by GLIB_000:8;
then A6: (the_Source_of (createGraph {0 ,1},{0 },S,T)) . 0 = 0 by FUNCOP_1:87;

now

given W being Walk of createGraph {0 ,1},{0 },S,T such that A7: W is Cycle-like ; :: thesis: contradiction

now

per cases ( len W = 3 or len W <> 3 ) ;

suppose A8: len W = 3 ; :: thesis: contradiction

set e = W . (1 + 1);
set v1 = W . 1;
set v2 = W . (1 + 2);
A9: W . (1 + 1) Joins W . 1,W . (1 + 2), createGraph {0 ,1},{0 },S,T by A8, GLIB_001:def 3, JORDAN12:3;
W . 1 = W . (1 + 2) by A7, A8, GLIB_001:119;
then A10: ( ( (the_Source_of (createGraph {0 ,1},{0 },S,T)) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph {0 ,1},{0 },S,T)) . (W . (1 + 1)) = W . 1 ) or ( (the_Source_of (createGraph {0 ,1},{0 },S,T)) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph {0 ,1},{0 },S,T)) . (W . (1 + 1)) = W . 1 ) ) by A9, GLIB_000:def 15;
W . (1 + 1) in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A9, GLIB_000:def 15;
then ( ( W . 1 = 0 & W . 1 = 1 ) or ( W . 1 = 1 & W . 1 = 0 ) ) by A4, A6, A5, A10, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

suppose A11: len W <> 3 ; :: thesis: contradiction

A12: 3 <= len W by A7, GLIB_001:126;
then 3 - 1 <= (len W) - 0 by XREAL_1:15;
then 2 * 1 in dom W by FINSEQ_3:27;
then W . (2 * 1) in {0 } by A4, GLIB_001:9;
then A13: W . (2 * 1) = 0 by TARSKI:def 1;
3 < len W by A11, A12, XXREAL_0:1;
then A14: 3 + 1 <= len W by NAT_1:13;
then 2 * 2 in dom W by FINSEQ_3:27;
then W . (2 * 2) in {0 } by A4, GLIB_001:9;
then W . (2 * 2) = 0 by TARSKI:def 1;
hence contradiction by A7, A14, A13, GLIB_001:139; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A15: createGraph {0 ,1},{0 },S,T is acyclic by Def2;
set W1 = (createGraph {0 ,1},{0 },S,T) .walkOf 0 ,0 ,1;
set W2 = ((createGraph {0 ,1},{0 },S,T) .walkOf 0 ,0 ,1) .reverse() ;
take createGraph {0 ,1},{0 },S,T ; :: thesis: ( not createGraph {0 ,1},{0 },S,T is trivial & createGraph {0 ,1},{0 },S,T is finite & createGraph {0 ,1},{0 },S,T is Tree-like )
A16: the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {0 ,1} by GLIB_000:8;
then reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph {0 ,1},{0 },S,T) by TARSKI:def 2;

now

assume card (the_Vertices_of (createGraph {0 ,1},{0 },S,T)) = 1 ; :: thesis: contradiction
then ex x being set st the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {x} by CARD_2:60;
hence contradiction by A16, ZFMISC_1:9; :: thesis: verum

end;

hence ( not createGraph {0 ,1},{0 },S,T is trivial & createGraph {0 ,1},{0 },S,T is finite ) by GLIB_000:def 21; :: thesis: createGraph {0 ,1},{0 },S,T is Tree-like
0 in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A4, TARSKI:def 1;
then 0 Joins 0 ,1, createGraph {0 ,1},{0 },S,T by A6, A5, GLIB_000:def 15;
then A17: (createGraph {0 ,1},{0 },S,T) .walkOf 0 ,0 ,1 is_Walk_from 0 ,1 by GLIB_001:16;
then A18: ((createGraph {0 ,1},{0 },S,T) .walkOf 0 ,0 ,1) .reverse() is_Walk_from 1, 0 by GLIB_001:24;

now

let u, v be Vertex of (createGraph {0 ,1},{0 },S,T); :: thesis: ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v

now

per cases ( ( u = 0 & v = 0 ) or ( u = 0 & v = 1 ) or ( u = 1 & v = 0 ) or ( u = 1 & v = 1 ) ) by A16, TARSKI:def 2;

suppose ( u = 0 & v = 0 ) ; :: thesis: ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v

then (createGraph {0 ,1},{0 },S,T) .walkOf a0 is_Walk_from u,v by GLIB_001:14;
hence ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v ; :: thesis: verum

end;

suppose ( u = 0 & v = 1 ) ; :: thesis: ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v

hence ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v by A17; :: thesis: verum

end;

suppose ( u = 1 & v = 0 ) ; :: thesis: ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v

hence ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v by A18; :: thesis: verum

end;

suppose ( u = 1 & v = 1 ) ; :: thesis: ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v

then (createGraph {0 ,1},{0 },S,T) .walkOf a1 is_Walk_from u,v by GLIB_001:14;
hence ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v ; :: thesis: verum

end;

end;

end;

hence ex W being Walk of createGraph {0 ,1},{0 },S,T st W is_Walk_from u,v ; :: thesis: verum

end;

then createGraph {0 ,1},{0 },S,T is connected by Def1;
hence createGraph {0 ,1},{0 },S,T is Tree-like by A15; :: thesis: verum