let G1, G2, G3 be _Graph; :: thesis: for G4 being LGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is LGraphComplement of G2
let G4 be LGraphComplement of G1; :: thesis: ( G1 == G2 & G3 == G4 implies G3 is LGraphComplement of G2 )
assume A1: ( G1 == G2 & G3 == G4 ) ; :: thesis: G3 is LGraphComplement of G2
then ( the_Vertices_of G4 = the_Vertices_of G3 & the_Edges_of G4 = the_Edges_of G3 ) by GLIB_000:def 34;
then ( the_Vertices_of G1 = the_Vertices_of G3 & the_Edges_of G3 misses the_Edges_of G1 ) by Def7;
then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 misses the_Edges_of G2 ) by A1, GLIB_000:def 34;
A3: G3 is non-multi by A1, GLIB_000:89;

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

let v, w be Vertex of G2; :: thesis: ( ( ex e1 being object st e1 Joins v,w,G2 implies for e2 being object holds not e2 Joins v,w,G3 ) & ( ( for e2 being object holds not e2 Joins v,w,G3 ) implies ex e1 being object st e1 Joins v,w,G2 ) )
A4: ( v is Vertex of G1 & w is Vertex of G1 ) by A1, GLIB_000:def 34;

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

given e1 being object such that A5: e1 Joins v,w,G2 ; :: thesis: for e2 being object holds not e2 Joins v,w,G3
e1 Joins v,w,G1 by A1, A5, GLIB_000:88;
then A6: for e2 being object holds not e2 Joins v,w,G4 by A4, Def7;
thus for e2 being object holds not e2 Joins v,w,G3 :: thesis: verum

proof

given e2 being object such that A7: e2 Joins v,w,G3 ; :: thesis: contradiction
e2 Joins v,w,G4 by A1, A7, GLIB_000:88;
hence contradiction by A6; :: thesis: verum

end;

end;

assume A8: for e2 being object holds not e2 Joins v,w,G3 ; :: thesis: ex e1 being object st e1 Joins v,w,G2
for e2 being object holds not e2 Joins v,w,G4

proof

given e2 being object such that A9: e2 Joins v,w,G4 ; :: thesis: contradiction
e2 Joins v,w,G3 by A1, A9, GLIB_000:88;
hence contradiction by A8; :: thesis: verum

end;

then consider e1 being object such that
A10: e1 Joins v,w,G1 by A4, Def7;
take e1 = e1; :: thesis: e1 Joins v,w,G2
thus e1 Joins v,w,G2 by A1, A10, GLIB_000:88; :: thesis: verum

end;

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