0 in {0} by TARSKI:def 1;
then reconsider f0 = NAT --> 0 as Function of NAT,{0} by FUNCOP_1:45;
set G = createGraph ({0},NAT,f0,f0);
A1: for n being Nat holds n DJoins 0 , 0 , createGraph ({0},NAT,f0,f0)
proof
let n be Nat; :: thesis: n DJoins 0 , 0 , createGraph ({0},NAT,f0,f0)
A2: n in NAT by ORDINAL1:def 12;
then A3: n in the_Edges_of (createGraph ({0},NAT,f0,f0)) ;
A4: (the_Source_of (createGraph ({0},NAT,f0,f0))) . n = f0 . n
.= 0 by A2, FUNCOP_1:7 ;
(the_Target_of (createGraph ({0},NAT,f0,f0))) . n = f0 . n
.= 0 by A2, FUNCOP_1:7 ;
hence n DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) by A3, A4, GLIB_000:def 14; :: thesis: verum
end;
take createGraph ({0},NAT,f0,f0) ; :: thesis: ( not createGraph ({0},NAT,f0,f0) is non-Dmulti & not createGraph ({0},NAT,f0,f0) is non-multi & not createGraph ({0},NAT,f0,f0) is loopless & not createGraph ({0},NAT,f0,f0) is Dsimple & not createGraph ({0},NAT,f0,f0) is simple & not createGraph ({0},NAT,f0,f0) is acyclic & not createGraph ({0},NAT,f0,f0) is _finite )
ex e1, e2, v1, v2 being object st
( e1 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & e2 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & e1 <> e2 )
proof
take 0 ; :: thesis: ex e2, v1, v2 being object st
( 0 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & e2 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & 0 <> e2 )
take 1 ; :: thesis: ex v1, v2 being object st
( 0 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & 1 DJoins v1,v2, createGraph ({0},NAT,f0,f0) & 0 <> 1 )
take 0 ; :: thesis: ex v2 being object st
( 0 DJoins 0 ,v2, createGraph ({0},NAT,f0,f0) & 1 DJoins 0 ,v2, createGraph ({0},NAT,f0,f0) & 0 <> 1 )
take 0 ; :: thesis: ( 0 DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) & 1 DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) & 0 <> 1 )
thus ( 0 DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) & 1 DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) & 0 <> 1 ) by A1; :: thesis: verum
end;
hence ( not createGraph ({0},NAT,f0,f0) is non-Dmulti & not createGraph ({0},NAT,f0,f0) is non-multi ) by GLIB_000:def 21; :: thesis: ( not createGraph ({0},NAT,f0,f0) is loopless & not createGraph ({0},NAT,f0,f0) is Dsimple & not createGraph ({0},NAT,f0,f0) is simple & not createGraph ({0},NAT,f0,f0) is acyclic & not createGraph ({0},NAT,f0,f0) is _finite )
ex e being object st
( e in the_Edges_of (createGraph ({0},NAT,f0,f0)) & (the_Source_of (createGraph ({0},NAT,f0,f0))) . e = (the_Target_of (createGraph ({0},NAT,f0,f0))) . e )
proof
take 0 ; :: thesis: ( 0 in the_Edges_of (createGraph ({0},NAT,f0,f0)) & (the_Source_of (createGraph ({0},NAT,f0,f0))) . 0 = (the_Target_of (createGraph ({0},NAT,f0,f0))) . 0 )
thus ( 0 in the_Edges_of (createGraph ({0},NAT,f0,f0)) & (the_Source_of (createGraph ({0},NAT,f0,f0))) . 0 = (the_Target_of (createGraph ({0},NAT,f0,f0))) . 0 ) ; :: thesis: verum
end;
hence ( not createGraph ({0},NAT,f0,f0) is loopless & not createGraph ({0},NAT,f0,f0) is Dsimple & not createGraph ({0},NAT,f0,f0) is simple ) ; :: thesis: ( not createGraph ({0},NAT,f0,f0) is acyclic & not createGraph ({0},NAT,f0,f0) is _finite )
set W = (createGraph ({0},NAT,f0,f0)) .walkOf (0,0,0);
0 DJoins 0 , 0 , createGraph ({0},NAT,f0,f0) by A1;
then 0 Joins 0 , 0 , createGraph ({0},NAT,f0,f0) by GLIB_000:16;
then (createGraph ({0},NAT,f0,f0)) .walkOf (0,0,0) is Cycle-like by GLIB_001:156;
hence not createGraph ({0},NAT,f0,f0) is acyclic ; :: thesis: not createGraph ({0},NAT,f0,f0) is _finite
not the_Edges_of (createGraph ({0},NAT,f0,f0)) is finite ;
hence not createGraph ({0},NAT,f0,f0) is _finite ; :: thesis: verum