let G1, G2 be _Graph; :: thesis: for G3 being SimpleGraph of G1
for G4 being SimpleGraph of G2
for G5 being GraphComplement of G1
for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
let G3 be SimpleGraph of G1; :: thesis: for G4 being SimpleGraph of G2
for G5 being GraphComplement of G1
for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
let G4 be SimpleGraph of G2; :: thesis: for G5 being GraphComplement of G1
for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
let G5 be GraphComplement of G1; :: thesis: for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
let G6 be GraphComplement of G2; :: thesis: ( G4 is G3 -isomorphic implies G6 is G5 -isomorphic )
A1: ( G5 is GraphComplement of G3 & G6 is GraphComplement of G4 ) by Th101;
assume G4 is G3 -isomorphic ; :: thesis: G6 is G5 -isomorphic
then consider f being PVertexMapping of G3,G4 such that
A2: f is isomorphism by GLIB_011:49;
A3: ( the_Vertices_of G3 = the_Vertices_of G5 & the_Vertices_of G4 = the_Vertices_of G6 ) by A1, Th98;
then reconsider g = f as PartFunc of (the_Vertices_of G5),(the_Vertices_of G6) ;

now :: thesis: for v, w, e being object st v in dom g & w in dom g & e Joins v,w,G5 holds
ex e6 being object st e6 Joins g . v,g . w,G6

let v, w, e be object ; :: thesis: ( v in dom g & w in dom g & e Joins v,w,G5 implies ex e6 being object st e6 Joins g . v,g . w,G6 )
assume A4: ( v in dom g & w in dom g & e Joins v,w,G5 ) ; :: thesis: ex e6 being object st e6 Joins g . v,g . w,G6
then A5: v <> w by GLIB_000:18;
then A6: g . v <> g . w by A2, A4, FUNCT_1:def 4;
A7: for e3 being object holds not e3 Joins v,w,G3 by A1, A3, A4, A5, Th98;
thus ex e6 being object st e6 Joins g . v,g . w,G6 :: thesis: verum

proof

assume A8: for e6 being object holds not e6 Joins g . v,g . w,G6 ; :: thesis: contradiction
( g . v in rng f & g . w in rng f ) by A4, FUNCT_1:3;
then consider e4 being object such that
A9: e4 Joins g . v,g . w,G4 by A1, A6, A8, Th98;
consider e3 being object such that
A10: e3 Joins v,w,G3 by A2, A4, A9, GLIB_011:2;
thus contradiction by A7, A10; :: thesis: verum

end;

end;

then reconsider g = g as PVertexMapping of G5,G6 by GLIB_011:1;

now :: thesis: for v, w, e6 being object st v in dom g & w in dom g & e6 Joins g . v,g . w,G6 holds
ex e5 being object st e5 Joins v,w,G5

let v, w, e6 be object ; :: thesis: ( v in dom g & w in dom g & e6 Joins g . v,g . w,G6 implies ex e5 being object st e5 Joins v,w,G5 )
assume A11: ( v in dom g & w in dom g & e6 Joins g . v,g . w,G6 ) ; :: thesis: ex e5 being object st e5 Joins v,w,G5
then A12: g . v <> g . w by GLIB_000:18;
A13: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by A3, A11;
( g . v in rng f & g . w in rng f ) by A11, FUNCT_1:3;
then A14: for e4 being object holds not e4 Joins g . v,g . w,G4 by A1, A11, A12, Th98;
thus ex e5 being object st e5 Joins v,w,G5 :: thesis: verum

proof

assume for e5 being object holds not e5 Joins v,w,G5 ; :: thesis: contradiction
then consider e3 being object such that
A15: e3 Joins v,w,G3 by A1, A12, A13, Th98;
consider e4 being object such that
A16: e4 Joins f . v,f . w,G4 by A11, A15, GLIB_011:1;
thus contradiction by A14, A16; :: thesis: verum

end;

end;

then g is continuous by GLIB_011:2;
hence G6 is G5 -isomorphic by A2, A3, GLIB_011:49; :: thesis: verum