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

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;

then reconsider S = 0 .--> 0 as Function of {0 },{0 ,1} by A1, FUNCT_2:5;

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;

then reconsider T = 0 .--> 1 as Function of {0 },{0 ,1} by A1, FUNCT_2:5;
set G = createGraph {0 ,1},{0 },S,T;
A2: ( the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {0 ,1} & the_Edges_of (createGraph {0 ,1},{0 },S,T) = {0 } & the_Source_of (createGraph {0 ,1},{0 },S,T) = S & the_Target_of (createGraph {0 ,1},{0 },S,T) = T ) by GLIB_000:8;
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 )

now

assume card (the_Vertices_of (createGraph {0 ,1},{0 },S,T)) = 1 ; :: thesis: contradiction
then consider x being set such that
A3: the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {x} by CARD_2:60;
thus contradiction by A2, A3, 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
reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph {0 ,1},{0 },S,T) by A2, TARSKI:def 2;
A4: 0 in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A2, TARSKI:def 1;
A5: ( (the_Source_of (createGraph {0 ,1},{0 },S,T)) . 0 = 0 & (the_Target_of (createGraph {0 ,1},{0 },S,T)) . 0 = 1 ) by A2, FUNCOP_1:87;
then A6: 0 Joins 0 ,1, createGraph {0 ,1},{0 },S,T by A4, GLIB_000:def 15;

now

given W being Walk of createGraph {0 ,1},{0 },S,T such that A7: W is Cycle-like ; :: thesis: contradiction
A8: ( W is closed & not W is trivial & W is Path-like ) by A7;
then A9: W is Trail-like ;

now

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

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

then A11: W . (1 + 1) Joins W . 1,W . (1 + 2), createGraph {0 ,1},{0 },S,T by GLIB_001:def 3, JORDAN12:3;
set e = W . (1 + 1);
set v1 = W . 1;
set v2 = W . (1 + 2);
W . 1 = W . (1 + 2) by A8, A10, GLIB_001:119;
then ( W . (1 + 1) in the_Edges_of (createGraph {0 ,1},{0 },S,T) & ( ( (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 A11, GLIB_000:def 15;
then ( ( W . 1 = 0 & W . 1 = 1 ) or ( W . 1 = 1 & W . 1 = 0 ) ) by A2, A5, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A16: 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() ;
A17: (createGraph {0 ,1},{0 },S,T) .walkOf 0 ,0 ,1 is_Walk_from 0 ,1 by A6, 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 A2, 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 A16; :: thesis: verum