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

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 simple & createGraph ({0,1},{0},S,T) is complete )

the_Source_of (createGraph ({0,1},{0},S,T)) = S by GLIB_000:6;

then A4: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 by FUNCOP_1:72;

A5: the_Edges_of (createGraph ({0,1},{0},S,T)) = {0} by GLIB_000:6;

A11: the_Vertices_of (createGraph ({0,1},{0},S,T)) = {0,1} by GLIB_000:6;

the_Target_of (createGraph ({0,1},{0},S,T)) = T by GLIB_000:6;

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

then A13: 0 Joins 0 ,1, createGraph ({0,1},{0},S,T) by A4, A12;

hence createGraph ({0,1},{0},S,T) is simple by A10; :: thesis: createGraph ({0,1},{0},S,T) is complete

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}

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;assume x in {0} ; :: thesis: (0 .--> 0) . 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

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

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 simple & createGraph ({0,1},{0},S,T) is complete )

the_Source_of (createGraph ({0,1},{0},S,T)) = S by GLIB_000:6;

then A4: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 by FUNCOP_1:72;

A5: the_Edges_of (createGraph ({0,1},{0},S,T)) = {0} by GLIB_000:6;

now :: thesis: 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 <> e2

then A10:
createGraph ({0,1},{0},S,T) is non-multi
;not e1 <> e2

let e1, e2, v1, v2 be object ; :: thesis: ( 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

A6: e1 Joins v1,v2, createGraph ({0,1},{0},S,T) and

A7: e2 Joins v1,v2, createGraph ({0,1},{0},S,T) ; :: thesis: not e1 <> e2

e1 in {0} by A5, A6;

then A8: e1 = 0 by TARSKI:def 1;

assume A9: e1 <> e2 ; :: thesis: contradiction

e2 in {0} by A5, A7;

hence contradiction by A9, A8, TARSKI:def 1; :: thesis: verum

end;assume that

A6: e1 Joins v1,v2, createGraph ({0,1},{0},S,T) and

A7: e2 Joins v1,v2, createGraph ({0,1},{0},S,T) ; :: thesis: not e1 <> e2

e1 in {0} by A5, A6;

then A8: e1 = 0 by TARSKI:def 1;

assume A9: e1 <> e2 ; :: thesis: contradiction

e2 in {0} by A5, A7;

hence contradiction by A9, A8, TARSKI:def 1; :: thesis: verum

A11: the_Vertices_of (createGraph ({0,1},{0},S,T)) = {0,1} by GLIB_000:6;

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 )
; :: thesis: ( createGraph ({0,1},{0},S,T) is simple & createGraph ({0,1},{0},S,T) is complete )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 A11, 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 A11, ZFMISC_1:5; :: thesis: verum

the_Target_of (createGraph ({0,1},{0},S,T)) = T by GLIB_000:6;

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

then A13: 0 Joins 0 ,1, createGraph ({0,1},{0},S,T) by A4, A12;

now :: thesis: for v, e being object holds not e Joins v,v, createGraph ({0,1},{0},S,T)

then
createGraph ({0,1},{0},S,T) is loopless
by GLIB_000:18;let v, e be object ; :: thesis: not e Joins v,v, createGraph ({0,1},{0},S,T)

assume A14: e Joins v,v, createGraph ({0,1},{0},S,T) ; :: thesis: contradiction

reconsider v = v as Vertex of (createGraph ({0,1},{0},S,T)) by A14, GLIB_000:13;

e in the_Edges_of (createGraph ({0,1},{0},S,T)) by A14;

then e Joins 0 ,1, createGraph ({0,1},{0},S,T) by A5, A13, TARSKI:def 1;

then ( ( 0 = v & 1 = v ) or ( 0 = v & 1 = v ) ) by A14;

hence contradiction ; :: thesis: verum

end;assume A14: e Joins v,v, createGraph ({0,1},{0},S,T) ; :: thesis: contradiction

reconsider v = v as Vertex of (createGraph ({0,1},{0},S,T)) by A14, GLIB_000:13;

e in the_Edges_of (createGraph ({0,1},{0},S,T)) by A14;

then e Joins 0 ,1, createGraph ({0,1},{0},S,T) by A5, A13, TARSKI:def 1;

then ( ( 0 = v & 1 = v ) or ( 0 = v & 1 = v ) ) by A14;

hence contradiction ; :: thesis: verum

hence createGraph ({0,1},{0},S,T) is simple by A10; :: thesis: createGraph ({0,1},{0},S,T) is complete

now :: thesis: for u, v being Vertex of (createGraph ({0,1},{0},S,T)) st u <> v holds

u,v are_adjacent

hence
createGraph ({0,1},{0},S,T) is complete
; :: thesis: verumu,v are_adjacent

let u, v be Vertex of (createGraph ({0,1},{0},S,T)); :: thesis: ( u <> v implies b_{1},b_{2} are_adjacent )

assume A15: u <> v ; :: thesis: b_{1},b_{2} are_adjacent

end;assume A15: u <> v ; :: thesis: b

per cases
( u = 0 or u = 1 )
by A11, TARSKI:def 2;

end;

suppose A16:
u = 0
; :: thesis: b_{1},b_{2} are_adjacent

A17:
0 in the_Edges_of (createGraph ({0,1},{0},S,T))
by A5, TARSKI:def 1;

v = 1 by A11, A15, A16, TARSKI:def 2;

then 0 Joins u,v, createGraph ({0,1},{0},S,T) by A4, A12, A16, A17;

hence u,v are_adjacent ; :: thesis: verum

end;v = 1 by A11, A15, A16, TARSKI:def 2;

then 0 Joins u,v, createGraph ({0,1},{0},S,T) by A4, A12, A16, A17;

hence u,v are_adjacent ; :: thesis: verum

suppose A18:
u = 1
; :: thesis: b_{1},b_{2} are_adjacent

A19:
0 in the_Edges_of (createGraph ({0,1},{0},S,T))
by A5, TARSKI:def 1;

v = 0 by A11, A15, A18, TARSKI:def 2;

then 0 Joins v,u, createGraph ({0,1},{0},S,T) by A4, A12, A18, A19;

hence u,v are_adjacent by Def3; :: thesis: verum

end;v = 0 by A11, A15, A18, TARSKI:def 2;

then 0 Joins v,u, createGraph ({0,1},{0},S,T) by A4, A12, A18, A19;

hence u,v are_adjacent by Def3; :: thesis: verum