let G be _Graph; :: thesis: ( G is 2 -edge & G is 2 -vertex & G is Dsimple implies ( G is 1 -Dregular & G is complete ) )
assume A1: ( G is 2 -edge & G is 2 -vertex & G is Dsimple ) ; :: thesis: ( G is 1 -Dregular & G is complete )
then G .order() = 2 by GLIB_013:def 3;
then consider v, w being object such that
A2: ( v <> w & {v,w} = the_Vertices_of G ) by CARD_2:60;
reconsider v = v, w = w as Vertex of G by A2, TARSKI:def 2;
ex e, f being object st
( e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G )

proof

G .size() = 2 by A1, GLIB_013:def 4;
then consider e1, e2 being object such that
A3: ( e1 <> e2 & {e1,e2} = the_Edges_of G ) by CARD_2:60;
A4: ( e1 in the_Edges_of G & e2 in the_Edges_of G ) by A3, TARSKI:def 2;
set x1 = (the_Source_of G) . e1;
set y1 = (the_Target_of G) . e1;
set x2 = (the_Source_of G) . e2;
set y2 = (the_Target_of G) . e2;
A5: ( e1 DJoins (the_Source_of G) . e1,(the_Target_of G) . e1,G & e2 DJoins (the_Source_of G) . e2,(the_Target_of G) . e2,G ) by A4, GLIB_000:def 14;
then A6: ( e1 Joins (the_Source_of G) . e1,(the_Target_of G) . e1,G & e2 Joins (the_Source_of G) . e2,(the_Target_of G) . e2,G ) by GLIB_000:16;
then reconsider x1 = (the_Source_of G) . e1, y1 = (the_Target_of G) . e1, x2 = (the_Source_of G) . e2, y2 = (the_Target_of G) . e2 as Vertex of G by GLIB_000:13;
A7: ( x1 <> y1 & x2 <> y2 ) by A1, A6, GLIB_000:18;
A8: ( x1 <> x2 or y1 <> y2 ) by A1, A3, A5, GLIB_000:def 21;
A9: ( ( x1 = v or x1 = w ) & ( y1 = v or y1 = w ) & ( x2 = v or x2 = w ) & ( y2 = v or y2 = w ) ) by A2, TARSKI:def 2;

per cases then ( ( x1 = v & y1 = w ) or ( x1 = w & y1 = v ) ) by A7;

suppose A10: ( x1 = v & y1 = w ) ; :: thesis: ex e, f being object st
( e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G )

take e1 ; :: thesis: ex f being object st
( e1 <> f & {e1,f} = the_Edges_of G & e1 DJoins v,w,G & f DJoins w,v,G )
take e2 ; :: thesis: ( e1 <> e2 & {e1,e2} = the_Edges_of G & e1 DJoins v,w,G & e2 DJoins w,v,G )
thus ( e1 <> e2 & {e1,e2} = the_Edges_of G ) by A3; :: thesis: ( e1 DJoins v,w,G & e2 DJoins w,v,G )
( x2 = w & y2 = v ) by A7, A8, A9, A10;
hence ( e1 DJoins v,w,G & e2 DJoins w,v,G ) by A5, A10; :: thesis: verum

end;

suppose A11: ( x1 = w & y1 = v ) ; :: thesis: ex e, f being object st
( e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G )

take e2 ; :: thesis: ex f being object st
( e2 <> f & {e2,f} = the_Edges_of G & e2 DJoins v,w,G & f DJoins w,v,G )
take e1 ; :: thesis: ( e2 <> e1 & {e2,e1} = the_Edges_of G & e2 DJoins v,w,G & e1 DJoins w,v,G )
thus ( e2 <> e1 & {e2,e1} = the_Edges_of G ) by A3; :: thesis: ( e2 DJoins v,w,G & e1 DJoins w,v,G )
( x2 = v & y2 = w ) by A7, A8, A9, A11;
hence ( e2 DJoins v,w,G & e1 DJoins w,v,G ) by A5, A11; :: thesis: verum

end;

end;

end;

then consider e, f being object such that
A12: ( e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G ) ;

now :: thesis: for x being object holds
( ( x in v .edgesIn() implies x = f ) & ( x = f implies x in v .edgesIn() ) )

let x be object ; :: thesis: ( ( x in v .edgesIn() implies x = f ) & ( x = f implies x in v .edgesIn() ) )

hereby :: thesis: ( x = f implies x in v .edgesIn() )

assume x in v .edgesIn() ; :: thesis: x = f
then consider z being set such that
A13: x DJoins z,v,G by GLIB_000:57;
x Joins z,v,G by A13, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then ( z = v or z = w ) by TARSKI:def 2;
then z = w by A1, A13, GLIB_000:136;
hence x = f by A1, A12, A13, GLIB_000:def 21; :: thesis: verum

end;

assume x = f ; :: thesis: x in v .edgesIn()
then ( x = f & f is set ) by TARSKI:1;
hence x in v .edgesIn() by A12, GLIB_000:57; :: thesis: verum

end;

then v .edgesIn() = {f} by TARSKI:def 1;
then A14: v .inDegree() = 1 by CARD_1:30;

now :: thesis: for x being object holds
( ( x in v .edgesOut() implies x = e ) & ( x = e implies x in v .edgesOut() ) )

let x be object ; :: thesis: ( ( x in v .edgesOut() implies x = e ) & ( x = e implies x in v .edgesOut() ) )

hereby :: thesis: ( x = e implies x in v .edgesOut() )

assume x in v .edgesOut() ; :: thesis: x = e
then consider z being set such that
A15: x DJoins v,z,G by GLIB_000:59;
x Joins v,z,G by A15, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then ( z = v or z = w ) by TARSKI:def 2;
then z = w by A1, A15, GLIB_000:136;
hence x = e by A1, A12, A15, GLIB_000:def 21; :: thesis: verum

end;

assume x = e ; :: thesis: x in v .edgesOut()
then ( x = e & e is set ) by TARSKI:1;
hence x in v .edgesOut() by A12, GLIB_000:59; :: thesis: verum

end;

then v .edgesOut() = {e} by TARSKI:def 1;
then A16: v .outDegree() = 1 by CARD_1:30;

now :: thesis: for x being object holds
( ( x in w .edgesIn() implies x = e ) & ( x = e implies x in w .edgesIn() ) )

let x be object ; :: thesis: ( ( x in w .edgesIn() implies x = e ) & ( x = e implies x in w .edgesIn() ) )

hereby :: thesis: ( x = e implies x in w .edgesIn() )

assume x in w .edgesIn() ; :: thesis: x = e
then consider z being set such that
A17: x DJoins z,w,G by GLIB_000:57;
x Joins z,w,G by A17, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then ( z = v or z = w ) by TARSKI:def 2;
then z = v by A1, A17, GLIB_000:136;
hence x = e by A1, A12, A17, GLIB_000:def 21; :: thesis: verum

end;

assume x = e ; :: thesis: x in w .edgesIn()
then ( x = e & e is set ) by TARSKI:1;
hence x in w .edgesIn() by A12, GLIB_000:57; :: thesis: verum

end;

then w .edgesIn() = {e} by TARSKI:def 1;
then A18: w .inDegree() = 1 by CARD_1:30;

now :: thesis: for x being object holds
( ( x in w .edgesOut() implies x = f ) & ( x = f implies x in w .edgesOut() ) )

let x be object ; :: thesis: ( ( x in w .edgesOut() implies x = f ) & ( x = f implies x in w .edgesOut() ) )

hereby :: thesis: ( x = f implies x in w .edgesOut() )

assume x in w .edgesOut() ; :: thesis: x = f
then consider z being set such that
A19: x DJoins w,z,G by GLIB_000:59;
x Joins w,z,G by A19, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then ( z = v or z = w ) by TARSKI:def 2;
then z = v by A1, A19, GLIB_000:136;
hence x = f by A1, A12, A19, GLIB_000:def 21; :: thesis: verum

end;

assume x = f ; :: thesis: x in w .edgesOut()
then ( x = f & f is set ) by TARSKI:1;
hence x in w .edgesOut() by A12, GLIB_000:59; :: thesis: verum

end;

then w .edgesOut() = {f} by TARSKI:def 1;
then A20: w .outDegree() = 1 by CARD_1:30;

now :: thesis: for u being Vertex of G holds
( u .inDegree() = 1 & u .outDegree() = 1 )

let u be Vertex of G; :: thesis: ( b₁ .inDegree() = 1 & b₁ .outDegree() = 1 )

per cases ( u = v or u = w ) by A2, TARSKI:def 2;

suppose u = v ; :: thesis: ( b₁ .inDegree() = 1 & b₁ .outDegree() = 1 )

hence ( u .inDegree() = 1 & u .outDegree() = 1 ) by A14, A16; :: thesis: verum

end;

suppose u = w ; :: thesis: ( b₁ .inDegree() = 1 & b₁ .outDegree() = 1 )

hence ( u .inDegree() = 1 & u .outDegree() = 1 ) by A18, A20; :: thesis: verum

end;

end;

end;

hence G is 1 -Dregular ; :: thesis: G is complete

now :: thesis: for x, y being Vertex of G st x <> y holds
x,y are_adjacent

let x, y be Vertex of G; :: thesis: ( x <> y implies x,y are_adjacent )
assume A21: x <> y ; :: thesis: x,y are_adjacent
( x in {v,w} & y in {v,w} ) by A2;
then ( ( x = v or x = w ) & ( y = v or y = w ) ) by TARSKI:def 2;
then e Joins x,y,G by A21, A12, GLIB_000:16;
hence x,y are_adjacent by CHORD:def 3; :: thesis: verum

end;

hence G is complete by CHORD:def 6; :: thesis: verum