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