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;
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;
verum
end;
take
createGraph ({0},NAT,f0,f0)
; ( 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
;
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
;
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
;
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
;
( 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;
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; ( 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
;
( 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 )
;
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 )
; ( 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
; 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
; verum