set V = {0,1};

set E = {0};

set S = 0 .--> 0;

set T = 0 .--> 1;

A1: dom (0 .--> 1) = {0} ;

dom (0 .--> 0) = {0} ;

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} ;

A5: (the_Target_of (createGraph ({0,1},{0},S,T))) . 0 = 1 by FUNCOP_1:72;

A6: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 ;

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 )

reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph ({0,1},{0},S,T)) by TARSKI:def 2;

0 in the_Edges_of (createGraph ({0,1},{0},S,T)) by 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;

hence createGraph ({0,1},{0},S,T) is Tree-like by A15; :: thesis: verum

set E = {0};

set S = 0 .--> 0;

set T = 0 .--> 1;

A1: dom (0 .--> 1) = {0} ;

A2: now :: thesis: for x being object st x in {0} holds

(0 .--> 1) . x in {0,1}

(0 .--> 1) . x in {0,1}

let x be object ; :: 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;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

A3: now :: thesis: for x being object st x in {0} holds

(0 .--> 0) . x in {0,1}

reconsider T = 0 .--> 1 as Function of {0},{0,1} by A1, A2, FUNCT_2:3;(0 .--> 0) . x in {0,1}

let x be object ; :: thesis: ( x in {0} implies (0 .--> 0) . x in {0,1} )

assume x in {0} ; :: thesis: (0 .--> 0) . x in {0,1}

(0 .--> 0) . x = 0 ;

hence (0 .--> 0) . x in {0,1} by TARSKI:def 2; :: thesis: verum

end;assume x in {0} ; :: thesis: (0 .--> 0) . x in {0,1}

(0 .--> 0) . x = 0 ;

hence (0 .--> 0) . x in {0,1} by TARSKI:def 2; :: thesis: verum

dom (0 .--> 0) = {0} ;

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} ;

A5: (the_Target_of (createGraph ({0,1},{0},S,T))) . 0 = 1 by FUNCOP_1:72;

A6: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 ;

now :: thesis: for W being Walk of createGraph ({0,1},{0},S,T) holds not W is Cycle-like

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

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( len W = 3 or len W <> 3 )
;

end;

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 A5, A10, TARSKI:def 1;

hence contradiction ; :: thesis: verum

end;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 A5, A10, TARSKI:def 1;

hence contradiction ; :: thesis: verum

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

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 )

reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph ({0,1},{0},S,T)) by TARSKI:def 2;

now :: thesis: not card (the_Vertices_of (createGraph ({0,1},{0},S,T))) = 1

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 assume
card (the_Vertices_of (createGraph ({0,1},{0},S,T))) = 1
; :: thesis: contradiction

then ex x being object st the_Vertices_of (createGraph ({0,1},{0},S,T)) = {x} by CARD_2:42;

hence contradiction by ZFMISC_1:5; :: thesis: verum

end;then ex x being object st the_Vertices_of (createGraph ({0,1},{0},S,T)) = {x} by CARD_2:42;

hence contradiction by ZFMISC_1:5; :: thesis: verum

0 in the_Edges_of (createGraph ({0,1},{0},S,T)) by 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 :: thesis: for u, v being Vertex of (createGraph ({0,1},{0},S,T)) 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) is connected
;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

end;now :: thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,vend;

hence
ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
; :: thesis: verumper cases
( ( u = 0 & v = 0 ) or ( u = 0 & v = 1 ) or ( u = 1 & v = 0 ) or ( u = 1 & v = 1 ) )
by TARSKI:def 2;

end;

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;hence ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v ; :: thesis: verum

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

end;

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

end;

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;hence ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v ; :: thesis: verum

hence createGraph ({0,1},{0},S,T) is Tree-like by A15; :: thesis: verum