set V = {0,1};
set E = {0};
set S = 0 .--> 0;
set T = 0 .--> 1;
A7:
dom (0 .--> 1) = {0}
;
reconsider T = 0 .--> 1 as Function of {0},{0,1} by A7, A8, FUNCT_2:3;
dom (0 .--> 0) = {0}
;
then reconsider S = 0 .--> 0 as Function of {0},{0,1} by A9, FUNCT_2:3;
set G = createGraph ({0,1},{0},S,T);
take
createGraph ({0,1},{0},S,T)
; ( not createGraph ({0,1},{0},S,T) is _trivial & createGraph ({0,1},{0},S,T) is _finite & createGraph ({0,1},{0},S,T) is simple & createGraph ({0,1},{0},S,T) is chordal )
A10:
(the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0
by FUNCOP_1:72;
hence
( not createGraph ({0,1},{0},S,T) is _trivial & createGraph ({0,1},{0},S,T) is _finite )
; ( createGraph ({0,1},{0},S,T) is simple & createGraph ({0,1},{0},S,T) is chordal )
A12:
(the_Target_of (createGraph ({0,1},{0},S,T))) . 0 = 1
by FUNCOP_1:72;
0 in the_Edges_of (createGraph ({0,1},{0},S,T))
by TARSKI:def 1;
then A14:
0 Joins 0 ,1, createGraph ({0,1},{0},S,T)
by A10, A12;
now for v, e being object holds not e Joins v,v, createGraph ({0,1},{0},S,T)let v,
e be
object ;
not e Joins v,v, createGraph ({0,1},{0},S,T)assume A15:
e Joins v,
v,
createGraph (
{0,1},
{0},
S,
T)
;
contradictionreconsider v =
v as
Vertex of
(createGraph ({0,1},{0},S,T)) by A15, GLIB_000:13;
e in the_Edges_of (createGraph ({0,1},{0},S,T))
by A15;
then
e Joins 0 ,1,
createGraph (
{0,1},
{0},
S,
T)
by A14, TARSKI:def 1;
then
( (
0 = v & 1
= v ) or (
0 = v & 1
= v ) )
by A15;
hence
contradiction
;
verum end;
then A16:
createGraph ({0,1},{0},S,T) is loopless
by GLIB_000:18;
now for e1, e2, v1, v2 being object st e1 Joins v1,v2, createGraph ({0,1},{0},S,T) & e2 Joins v1,v2, createGraph ({0,1},{0},S,T) holds
not e1 <> e2let e1,
e2,
v1,
v2 be
object ;
( e1 Joins v1,v2, createGraph ({0,1},{0},S,T) & e2 Joins v1,v2, createGraph ({0,1},{0},S,T) implies not e1 <> e2 )assume that A17:
e1 Joins v1,
v2,
createGraph (
{0,1},
{0},
S,
T)
and A18:
e2 Joins v1,
v2,
createGraph (
{0,1},
{0},
S,
T)
;
not e1 <> e2
e1 in {0}
by A17;
then A19:
e1 = 0
by TARSKI:def 1;
assume A20:
e1 <> e2
;
contradiction
e2 in {0}
by A18;
hence
contradiction
by A20, A19, TARSKI:def 1;
verum end;
then
createGraph ({0,1},{0},S,T) is non-multi
;
hence
createGraph ({0,1},{0},S,T) is simple
by A16; createGraph ({0,1},{0},S,T) is chordal
card (the_Vertices_of (createGraph ({0,1},{0},S,T))) = 2
by CARD_2:57;
hence
createGraph ({0,1},{0},S,T) is chordal
by Th95; verum