let G be _Graph; :: thesis: ( G is 1 -regular & G is connected implies ( G is 2 -vertex & G is 1 -edge & G is complete ) )
assume A1: ( G is 1 -regular & G is connected ) ; :: thesis: ( G is 2 -vertex & G is 1 -edge & G is complete )
set v = the Vertex of G;
consider e being object such that
A2: ( the Vertex of G .edgesInOut() = {e} & not e Joins the Vertex of G, the Vertex of G,G ) by A1, GLIB_000:def 51;
A3: e in the Vertex of G .edgesInOut() by A2, TARSKI:def 1;
then A4: e in the_Edges_of G ;
ex w being Vertex of G st
( w <> the Vertex of G & e Joins the Vertex of G,w,G )

proof

set x = (the_Source_of G) . e;
set y = (the_Target_of G) . e;
A5: ( e Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e Joins (the_Target_of G) . e,(the_Source_of G) . e,G ) by A4, GLIB_000:def 13;
then reconsider x = (the_Source_of G) . e, y = (the_Target_of G) . e as Vertex of G by GLIB_000:13;

per cases ( the Vertex of G = x or the Vertex of G = y ) by A3, GLIB_000:61;

suppose A6: the Vertex of G = x ; :: thesis: ex w being Vertex of G st
( w <> the Vertex of G & e Joins the Vertex of G,w,G )

take y ; :: thesis: ( y <> the Vertex of G & e Joins the Vertex of G,y,G )
thus ( y <> the Vertex of G & e Joins the Vertex of G,y,G ) by A2, A5, A6; :: thesis: verum

end;

suppose A7: the Vertex of G = y ; :: thesis: ex w being Vertex of G st
( w <> the Vertex of G & e Joins the Vertex of G,w,G )

take x ; :: thesis: ( x <> the Vertex of G & e Joins the Vertex of G,x,G )
thus ( x <> the Vertex of G & e Joins the Vertex of G,x,G ) by A2, A5, A7; :: thesis: verum

end;

end;

end;

then consider w being Vertex of G such that
A8: ( w <> the Vertex of G & e Joins the Vertex of G,w,G ) ;

now :: thesis: for x being object holds
( ( x in the_Vertices_of G & x <> the Vertex of G implies not x <> w ) & ( ( x = the Vertex of G or x = w ) implies x in the_Vertices_of G ) )

let x be object ; :: thesis: ( ( x in the_Vertices_of G & x <> the Vertex of G implies not x <> w ) & ( ( x = the Vertex of G or x = w ) implies x in the_Vertices_of G ) )

hereby :: thesis: ( ( x = the Vertex of G or x = w ) implies x in the_Vertices_of G )

assume x in the_Vertices_of G ; :: thesis: ( x <> the Vertex of G implies not x <> w )
then reconsider u = x as Vertex of G ;
assume A9: ( x <> the Vertex of G & x <> w ) ; :: thesis: contradiction
consider W being Walk of G such that
A10: W is_Walk_from the Vertex of G,u by A1, GLIB_002:def 1;
set P = the Path of W;
the Path of W is_Walk_from the Vertex of G,u by A10, GLIB_001:160;
then A11: ( the Path of W .first() = the Vertex of G & the Path of W .last() = u ) by GLIB_001:def 23;
then A12: the Path of W is trivial by A9, GLIB_001:127;
then consider e1 being object such that
e1 Joins the Path of W .first() , the Path of W .last() ,G and
A13: the Path of W = G .walkOf (( the Path of W .first()),e1,( the Path of W .last())) by A1, Th29;
A14: the Path of W = G .walkOf ( the Vertex of G,e1,u) by A11, A13;
G .walkOf the Vertex of G is trivial ;
then A15: e1 Joins the Vertex of G,u,G by A12, A14, GLIB_001:def 5;
then e1 in the Vertex of G .edgesInOut() by GLIB_000:62;
then e1 = e by A2, TARSKI:def 1;
hence contradiction by A8, A9, A15, GLIB_000:15; :: thesis: verum

end;

assume ( x = the Vertex of G or x = w ) ; :: thesis: x in the_Vertices_of G
hence x in the_Vertices_of G ; :: thesis: verum

end;

then A16: the_Vertices_of G = { the Vertex of G,w} by TARSKI:def 2;
then G .order() = 2 by A8, CARD_2:57;
hence G is 2 -vertex by GLIB_013:def 3; :: thesis: ( G is 1 -edge & G is complete )

now :: thesis: for x being object holds
( ( x in the_Edges_of G implies x = e ) & ( x = e implies x in the_Edges_of G ) )

let x be object ; :: thesis: ( ( x in the_Edges_of G implies x = e ) & ( x = e implies x in the_Edges_of G ) )

hereby :: thesis: ( x = e implies x in the_Edges_of G )

set y = (the_Source_of G) . x;
set z = (the_Target_of G) . x;
assume x in the_Edges_of G ; :: thesis: x = e
then A17: x Joins (the_Source_of G) . x,(the_Target_of G) . x,G by GLIB_000:def 13;
then ( (the_Source_of G) . x in { the Vertex of G,w} & (the_Target_of G) . x in { the Vertex of G,w} ) by A16, GLIB_000:13;

per cases then ( (the_Source_of G) . x = the Vertex of G or (the_Target_of G) . x = the Vertex of G or ( (the_Source_of G) . x = w & (the_Target_of G) . x = w ) ) by TARSKI:def 2;

suppose ( (the_Source_of G) . x = the Vertex of G or (the_Target_of G) . x = the Vertex of G ) ; :: thesis: x = e

then x in the Vertex of G .edgesInOut() by A17, GLIB_000:14, GLIB_000:62;
hence x = e by A2, TARSKI:def 1; :: thesis: verum

end;

suppose ( (the_Source_of G) . x = w & (the_Target_of G) . x = w ) ; :: thesis: x = e

hence x = e by A1, A17, GLIB_000:146; :: thesis: verum

end;

end;

end;

assume x = e ; :: thesis: x in the_Edges_of G
hence x in the_Edges_of G by A4; :: thesis: verum

end;

then the_Edges_of G = {e} by TARSKI:def 1;
then G .size() = 1 by CARD_1:30;
hence G is 1 -edge by GLIB_013:def 4; :: 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 A18: x <> y ; :: thesis: x,y are_adjacent
( ( x = the Vertex of G or x = w ) & ( y = the Vertex of G or y = w ) ) by A16, TARSKI:def 2;
then ( ( x = the Vertex of G & y = w ) or ( x = w & y = the Vertex of G ) ) by A18;
hence x,y are_adjacent by A8, CHORD:def 3; :: thesis: verum

end;

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