let G1 be non _trivial connected _Graph; :: thesis:
let G2 be non spanning Subgraph of G1; :: thesis:
set S = the_Vertices_of G2;
A1: the_Vertices_of G2 is non empty proper Subset of (the_Vertices_of G1) by GLIB_000:def 33, SUBSET_1:def 6;
set v0 = the Element of G1 .AdjacentSet (the_Vertices_of G2);
reconsider v0 = the Element of G1 .AdjacentSet (the_Vertices_of G2) as Vertex of G1 by A1, TARSKI:def 3;
consider w0 being Vertex of G1 such that
A2: ( w0 in the_Vertices_of G2 & v0,w0 are_adjacent ) by A1, CHORD:50;
consider e being object such that
A3: e Joins v0,w0,G1 by A2, CHORD:def 3;
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
take (the_Source_of G1) . e ; :: thesis:
take e ; :: thesis:
take (the_Target_of G1) . e ; :: thesis:
A4: e in the_Edges_of G1 by A3, GLIB_000:def 13;
then A5: ( e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 & e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 ) by GLIB_000:def 13, GLIB_000:def 14;
then A6: ( ( (the_Source_of G1) . e = v0 & (the_Target_of G1) . e = w0 ) or ( (the_Source_of G1) . e = w0 & (the_Target_of G1) . e = v0 ) ) by A3, GLIB_000:15;
A7: not v0 in the_Vertices_of G2 by A1, CHORD:50;
hence ( (the_Source_of G1) . e <> (the_Target_of G1) . e & e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 ) by A2, A5, A6; :: thesis:
thus A8: not e in the_Edges_of G2 :: thesis:

assume e in the_Edges_of G2 ; :: thesis:
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G2 by A5, GLIB_000:73;
hence contradiction by A6, A7, GLIB_000:13; :: thesis:

end;

hereby :: thesis:

let G3 be addAdjVertex of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e; :: thesis:

( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in the_Vertices_of G1 ) by A5, GLIB_000:13;
then A9: {((the_Source_of G1) . e),((the_Target_of G1) . e)} c= the_Vertices_of G1 by ZFMISC_1:32;
A10: (the_Vertices_of G2) \/ {((the_Source_of G1) . e),((the_Target_of G1) . e)} c= the_Vertices_of G1 by A9, XBOOLE_1:8;
the_Vertices_of G3 c= (the_Vertices_of G2) \/ {((the_Source_of G1) . e),((the_Target_of G1) . e)} by Th54;
hence the_Vertices_of G3 c= the_Vertices_of G1 by A10, XBOOLE_1:1; :: thesis:
A11: {e} c= the_Edges_of G1 by A4, ZFMISC_1:31;
A12: (the_Edges_of G2) \/ {e} c= the_Edges_of G1 by A11, XBOOLE_1:8;
A13: the_Edges_of G3 c= (the_Edges_of G2) \/ {e} by Th54;
hence the_Edges_of G3 c= the_Edges_of G1 by A12, XBOOLE_1:1; :: thesis:
let e0 be set ; :: thesis:
assume e0 in the_Edges_of G3 ; :: thesis:

per cases by A13, ZFMISC_1:136;

suppose A14: e0 in the_Edges_of G2 ; :: thesis:

hence (the_Source_of G3) . e0 = (the_Source_of G2) . e0 by GLIB_006:def 9
.= (the_Source_of G1) . e0 by A14, GLIB_000:def 32 ;
:: thesis:
thus (the_Target_of G3) . e0 = (the_Target_of G2) . e0 by A14, GLIB_006:def 9
.= (the_Target_of G1) . e0 by A14, GLIB_000:def 32 ; :: thesis:

end;

suppose A15: e0 = e ; :: thesis:

A16: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G3 by A2, A6, A7, A8, GLIB_006:131, GLIB_006:132;
hence (the_Source_of G3) . e0 = (the_Source_of G1) . e0 by A15, GLIB_000:def 14; :: thesis:
thus (the_Target_of G3) . e0 = (the_Target_of G1) . e0 by A15, A16, GLIB_000:def 14; :: thesis:

end;

end;

end;

hence G3 is Subgraph of G1 by GLIB_000:def 32; :: thesis:

end;

thus ( ( (the_Source_of G1) . e in the_Vertices_of G2 & not (the_Target_of G1) . e in the_Vertices_of G2 ) or ( not (the_Source_of G1) . e in the_Vertices_of G2 & (the_Target_of G1) . e in the_Vertices_of G2 ) ) by A2, A6, A7; :: thesis: