set V = {0 ,1};
set E = {0 };
set S = 0 .--> 0 ;
set T = 0 .--> 1;
A1: ( dom (0 .--> 0 ) = {0 } & dom (0 .--> 1) = {0 } ) by FUNCOP_1:19;

now

let x be set ; :: 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:87;
hence (0 .--> 0 ) . x in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

then reconsider S = 0 .--> 0 as Function of {0 },{0 ,1} by A1, FUNCT_2:5;

now

let x be set ; :: 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:87;
hence (0 .--> 1) . x in {0 ,1} by TARSKI:def 2; :: thesis: verum

end;

then reconsider T = 0 .--> 1 as Function of {0 },{0 ,1} by A1, FUNCT_2:5;
set G = createGraph {0 ,1},{0 },S,T;
A2: ( the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {0 ,1} & the_Edges_of (createGraph {0 ,1},{0 },S,T) = {0 } & the_Source_of (createGraph {0 ,1},{0 },S,T) = S & the_Target_of (createGraph {0 ,1},{0 },S,T) = T ) by GLIB_000:8;
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 )

now

assume card (the_Vertices_of (createGraph {0 ,1},{0 },S,T)) = 1 ; :: thesis: contradiction
then consider x being set such that
A3: the_Vertices_of (createGraph {0 ,1},{0 },S,T) = {x} by CARD_2:60;
thus contradiction by A2, A3, ZFMISC_1:9; :: thesis: verum

end;

hence ( not createGraph {0 ,1},{0 },S,T is trivial & createGraph {0 ,1},{0 },S,T is finite ) by GLIB_000:def 21; :: thesis: ( createGraph {0 ,1},{0 },S,T is simple & createGraph {0 ,1},{0 },S,T is complete )
A4: (the_Source_of (createGraph {0 ,1},{0 },S,T)) . 0 = 0 by A2, FUNCOP_1:87;
A5: (the_Target_of (createGraph {0 ,1},{0 },S,T)) . 0 = 1 by A2, FUNCOP_1:87;
0 in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A2, TARSKI:def 1;
then A6: 0 Joins 0 ,1, createGraph {0 ,1},{0 },S,T by A4, A5, GLIB_000:def 15;

now

let v, e be set ; :: thesis: not e Joins v,v, createGraph {0 ,1},{0 },S,T
assume A7: 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 A7, GLIB_000:16;
e in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A7, GLIB_000:def 15;
then e Joins 0 ,1, createGraph {0 ,1},{0 },S,T by A2, A6, TARSKI:def 1;
then ( ( 0 = v & 1 = v ) or ( 0 = v & 1 = v ) ) by A7, GLIB_000:18;
hence contradiction ; :: thesis: verum

end;

then A8: createGraph {0 ,1},{0 },S,T is loopless by GLIB_000:21;

now

let e1, e2, v1, v2 be set ; :: 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 A9: ( e1 Joins v1,v2, createGraph {0 ,1},{0 },S,T & e2 Joins v1,v2, createGraph {0 ,1},{0 },S,T ) ; :: thesis: not e1 <> e2
assume A10: e1 <> e2 ; :: thesis: contradiction
( e1 in {0 } & e2 in {0 } ) by A2, A9, GLIB_000:def 15;
then ( e1 = 0 & e2 = 0 ) by TARSKI:def 1;
hence contradiction by A10; :: thesis: verum

end;

then createGraph {0 ,1},{0 },S,T is non-multi by GLIB_000:def 22;
hence createGraph {0 ,1},{0 },S,T is simple by A8; :: thesis: createGraph {0 ,1},{0 },S,T is complete

now

let u, v be Vertex of (createGraph {0 ,1},{0 },S,T); :: thesis: ( u <> v implies b₁,b₂ are_adjacent )
assume A11: u <> v ; :: thesis: b₁,b₂ are_adjacent

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

suppose A12: u = 0 ; :: thesis: b₁,b₂ are_adjacent

then A13: v = 1 by A2, A11, TARSKI:def 2;
0 in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A2, TARSKI:def 1;
then 0 Joins u,v, createGraph {0 ,1},{0 },S,T by A4, A5, A12, A13, GLIB_000:def 15;
hence u,v are_adjacent by Def3; :: thesis: verum

end;

suppose A14: u = 1 ; :: thesis: b₁,b₂ are_adjacent

then A15: v = 0 by A2, A11, TARSKI:def 2;
0 in the_Edges_of (createGraph {0 ,1},{0 },S,T) by A2, TARSKI:def 1;
then 0 Joins v,u, createGraph {0 ,1},{0 },S,T by A4, A5, A14, A15, GLIB_000:def 15;
hence u,v are_adjacent by Def3; :: thesis: verum

end;

end;

end;

hence createGraph {0 ,1},{0 },S,T is complete by Def6; :: thesis: verum