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

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:72;
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:72;
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:3;
dom (0 .--> 0) = {0} by FUNCOP_1:13;
then reconsider S = 0 .--> 0 as Function of {0},{0,1} by A3, FUNCT_2:3;
set G = createGraph ({0,1},{0},S,T);
A4: the_Edges_of (createGraph ({0,1},{0},S,T)) = {0} by GLIB_000:6;
the_Target_of (createGraph ({0,1},{0},S,T)) = T by GLIB_000:6;
then A5: (the_Target_of (createGraph ({0,1},{0},S,T))) . 0 = 1 by FUNCOP_1:72;
the_Source_of (createGraph ({0,1},{0},S,T)) = S by GLIB_000:6;
then A6: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 by FUNCOP_1:72;

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:2;
W . 1 = W . (1 + 2) by A7, A8, GLIB_001:118;
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 13;
W . (1 + 1) in the_Edges_of (createGraph ({0,1},{0},S,T)) by A9, GLIB_000:def 13;
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:125;
then 3 - 1 <= (len W) - 0 by XREAL_1:13;
then 2 * 1 in dom W by FINSEQ_3:25;
then W . (2 * 1) in {0} by A4, GLIB_001:8;
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:25;
then W . (2 * 2) in {0} by A4, GLIB_001:8;
then W . (2 * 2) = 0 by TARSKI:def 1;
hence contradiction by A7, A14, A13, GLIB_001:138; :: 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:6;
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:42;
hence contradiction by A16, ZFMISC_1:5; :: 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 19; :: 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 13;
then A17: (createGraph ({0,1},{0},S,T)) .walkOf (0,0,1) is_Walk_from 0 ,1 by GLIB_001:15;
then A18: ((createGraph ({0,1},{0},S,T)) .walkOf (0,0,1)) .reverse() is_Walk_from 1, 0 by GLIB_001:23;

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:13;
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:13;
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