let G be _Graph; :: thesis: ( G is simple & G is 2 -vertex & G is connected implies G is 1 -regular )
assume A19: ( G is simple & G is 2 -vertex & G is connected ) ; :: thesis: G is 1 -regular
then G .order() = 2 by GLIB_013:def 3;
then consider v, w being object such that
A20: ( v <> w & the_Vertices_of G = {v,w} ) by CARD_2:60;
reconsider v = v, w = w as Vertex of G by A20, TARSKI:def 2;
consider W being Walk of G such that
A21: W is_Walk_from v,w by A19, GLIB_002:def 1;
set P = the Path of W;
the Path of W is_Walk_from v,w by A21, GLIB_001:160;
then A22: ( the Path of W .first() = v & the Path of W .last() = w ) by GLIB_001:def 23;
then ( 3 <= len the Path of W & 1 < 3 ) by A20, GLIB_001:125, GLIB_001:127;
then 1 < len the Path of W by XXREAL_0:2;
then A23: the Path of W . (1 + 1) Joins the Path of W . 1, the Path of W . (1 + 2),G by GLIB_001:def 3, POLYFORM:4;
then A24: the Path of W . 3 in the_Vertices_of G by GLIB_000:13;
set e = the Path of W . 2;
A25: the Path of W . 1 = v by A22, GLIB_001:def 6;
then the Path of W . 3 <> v by A19, A23, GLIB_000:18;
then A26: the Path of W . 2 Joins v,w,G by A20, A23, A24, A25, TARSKI:def 2;

now :: thesis: for f being object holds
( ( f in v .edgesInOut() implies f = the Path of W . 2 ) & ( f = the Path of W . 2 implies f in v .edgesInOut() ) )

let f be object ; :: thesis: ( ( f in v .edgesInOut() implies f = the Path of W . 2 ) & ( f = the Path of W . 2 implies f in v .edgesInOut() ) )

hereby :: thesis: ( f = the Path of W . 2 implies f in v .edgesInOut() )

assume f in v .edgesInOut() ; :: thesis: f = the Path of W . 2
then consider u being Vertex of G such that
A27: f Joins v,u,G by GLIB_000:64;
u <> v by A19, A27, GLIB_000:18;
then u = w by A20, TARSKI:def 2;
hence f = the Path of W . 2 by A19, A26, A27, GLIB_000:def 20; :: thesis: verum

end;

assume f = the Path of W . 2 ; :: thesis: f in v .edgesInOut()
hence f in v .edgesInOut() by A26, GLIB_000:62; :: thesis: verum

end;

then v .edgesInOut() = {( the Path of W . 2)} by TARSKI:def 1;
then v is endvertex by A19, GLIB_000:18, GLIB_000:def 51;
then A28: v .degree() = 1 by GLIB_000:174;

now :: thesis: for f being object holds
( ( f in w .edgesInOut() implies f = the Path of W . 2 ) & ( f = the Path of W . 2 implies f in w .edgesInOut() ) )

let f be object ; :: thesis: ( ( f in w .edgesInOut() implies f = the Path of W . 2 ) & ( f = the Path of W . 2 implies f in w .edgesInOut() ) )

hereby :: thesis: ( f = the Path of W . 2 implies f in w .edgesInOut() )

assume f in w .edgesInOut() ; :: thesis: f = the Path of W . 2
then consider u being Vertex of G such that
A29: f Joins w,u,G by GLIB_000:64;
A30: f Joins u,w,G by A29, GLIB_000:14;
u <> w by A19, A29, GLIB_000:18;
then u = v by A20, TARSKI:def 2;
hence f = the Path of W . 2 by A19, A26, A30, GLIB_000:def 20; :: thesis: verum

end;

assume f = the Path of W . 2 ; :: thesis: f in w .edgesInOut()
hence f in w .edgesInOut() by A26, GLIB_000:14, GLIB_000:62; :: thesis: verum

end;

then w .edgesInOut() = {( the Path of W . 2)} by TARSKI:def 1;
then w is endvertex by A19, GLIB_000:18, GLIB_000:def 51;
then A31: w .degree() = 1 by GLIB_000:174;
let u be Vertex of G; :: according to GLIB_016:def 4 :: thesis: u .degree() = 1

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

suppose u = v ; :: thesis: u .degree() = 1

hence u .degree() = 1 by A28; :: thesis: verum

end;

suppose u = w ; :: thesis: u .degree() = 1

hence u .degree() = 1 by A31; :: thesis: verum

end;

end;