let G1 be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being LGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2
let V be non empty Subset of (the_Vertices_of G1); :: thesis: for G2 being inducedSubgraph of G1,V
for G3 being LGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2
let G2 be inducedSubgraph of G1,V; :: thesis: for G3 being LGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2
let G3 be LGraphComplement of G1; :: thesis: for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2
let G4 be inducedSubgraph of G3,V; :: thesis: G4 is LGraphComplement of G2
A1: V is non empty Subset of (the_Vertices_of G3) by Def7;
then A2: the_Vertices_of G4 = V by GLIB_000:def 37
.= the_Vertices_of G2 by GLIB_000:def 37 ;
A3: the_Edges_of G4 misses the_Edges_of G2

proof

assume the_Edges_of G4 meets the_Edges_of G2 ; :: thesis: contradiction
then consider e being object such that
A4: ( e in the_Edges_of G4 & e in the_Edges_of G2 ) by XBOOLE_0:3;
A5: e in (the_Edges_of G1) \/ (the_Edges_of G3) by A4, XBOOLE_0:def 3;
the_Edges_of G3 misses the_Edges_of G1 by Def7;
hence contradiction by A4, A5, XBOOLE_0:5; :: thesis: verum

end;

now :: thesis: for v, w being Vertex of G2 holds
( ( ex e2 being object st e2 Joins v,w,G2 implies for e4 being object holds not e4 Joins v,w,G4 ) & ( ( for e4 being object holds not e4 Joins v,w,G4 ) implies ex e1 being object st e1 Joins v,w,G2 ) )

let v, w be Vertex of G2; :: thesis: ( ( ex e2 being object st e2 Joins v,w,G2 implies for e4 being object holds not e4 Joins v,w,G4 ) & ( ( for e4 being object holds not e4 Joins v,w,G4 ) implies ex e1 being object st e1 Joins v,w,G2 ) )

hereby :: thesis: ( ( for e4 being object holds not e4 Joins v,w,G4 ) implies ex e1 being object st e1 Joins v,w,G2 )

given e2 being object such that A6: e2 Joins v,w,G2 ; :: thesis: for e4 being object holds not e4 Joins v,w,G4
A7: e2 Joins v,w,G1 by A6, GLIB_000:72;
given e4 being object such that A8: e4 Joins v,w,G4 ; :: thesis: contradiction
e4 Joins v,w,G3 by A8, GLIB_000:72;
hence contradiction by A7, Th64; :: thesis: verum

end;

assume A9: for e4 being object holds not e4 Joins v,w,G4 ; :: thesis: ex e1 being object st e1 Joins v,w,G2
ex e1 being object st e1 Joins v,w,G1

proof

assume A10: for e1 being object holds not e1 Joins v,w,G1 ; :: thesis: contradiction
the_Vertices_of G2 c= the_Vertices_of G1 ;
then ( v is Vertex of G1 & w is Vertex of G1 ) by TARSKI:def 3;
then consider e3 being object such that
A11: e3 Joins v,w,G3 by A10, Def7;
the_Vertices_of G2 = V by GLIB_000:def 37;
then e3 in G3 .edgesBetween V by A11, GLIB_000:32;
then ( e3 in the_Edges_of G4 & e3 is set ) by A1, GLIB_000:def 37;
then e3 Joins v,w,G4 by A11, GLIB_000:73;
hence contradiction by A9; :: thesis: verum

end;

then consider e1 being object such that
A12: e1 Joins v,w,G1 ;
take e1 = e1; :: thesis: e1 Joins v,w,G2
the_Vertices_of G2 = V by GLIB_000:def 37;
then e1 in G1 .edgesBetween V by A12, GLIB_000:32;
then ( e1 in the_Edges_of G2 & e1 is set ) by GLIB_000:def 37;
hence e1 Joins v,w,G2 by A12, GLIB_000:73; :: thesis: verum

end;

hence G4 is LGraphComplement of G2 by A2, A3, Def7; :: thesis: verum