let G1 be _Graph; for G2 being simple _Graph holds
( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )
let G2 be simple _Graph; ( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )
hereby ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) implies G2 is GraphComplement of G1 )
assume A1:
G2 is
GraphComplement of
G1
;
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) ) ) )hence
(
the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 misses the_Edges_of G1 )
by Th98;
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )let v1,
w1 be
Vertex of
G1;
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )let v2,
w2 be
Vertex of
G2;
( v1 = v2 & w1 = w2 & v1 <> w1 implies ( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) ) )assume A2:
(
v1 = v2 &
w1 = w2 &
v1 <> w1 )
;
( ( v1,w1 are_adjacent implies not v2,w2 are_adjacent ) & ( not v2,w2 are_adjacent implies v1,w1 are_adjacent ) )hereby ( not v2,w2 are_adjacent implies v1,w1 are_adjacent )
assume
v1,
w1 are_adjacent
;
not v2,w2 are_adjacent then
ex
e1 being
object st
e1 Joins v1,
w1,
G1
by CHORD:def 3;
then
for
e2 being
object holds not
e2 Joins v1,
w1,
G2
by A1, A2, Th98;
hence
not
v2,
w2 are_adjacent
by A2, CHORD:def 3;
verum
end; assume
not
v2,
w2 are_adjacent
;
v1,w1 are_adjacent then
for
e2 being
object holds not
e2 Joins v1,
w1,
G2
by A2, CHORD:def 3;
then
ex
e1 being
object st
e1 Joins v1,
w1,
G1
by A1, A2, Th98;
hence
v1,
w1 are_adjacent
by CHORD:def 3;
verum
end;
assume that
A3:
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 )
and
A4:
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent )
; G2 is GraphComplement of G1
now for v1, w1 being Vertex of G1 st v1 <> w1 holds
( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) )let v1,
w1 be
Vertex of
G1;
( v1 <> w1 implies ( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) ) )assume A5:
v1 <> w1
;
( ( ex e1 being object st e1 Joins v1,w1,G1 implies for e2 being object holds not e2 Joins v1,w1,G2 ) & ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 ) )reconsider v2 =
v1,
w2 =
w1 as
Vertex of
G2 by A3;
hereby ( ( for e2 being object holds not e2 Joins v1,w1,G2 ) implies ex e1 being object st e1 Joins v1,w1,G1 )
end; assume
for
e2 being
object holds not
e2 Joins v1,
w1,
G2
;
ex e1 being object st e1 Joins v1,w1,G1then
not
v2,
w2 are_adjacent
by CHORD:def 3;
then
v1,
w1 are_adjacent
by A5, A4;
hence
ex
e1 being
object st
e1 Joins v1,
w1,
G1
by CHORD:def 3;
verum end;
hence
G2 is GraphComplement of G1
by A3, Th98; verum