let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )
let V be set ; for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )
let G1 be addAdjVertexAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies ( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) ) )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; ( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )
hereby ( G2 is complete & V = the_Vertices_of G2 implies G1 is complete )
assume A2:
G1 is
complete
;
( G2 is complete & V = the_Vertices_of G2 )
for
u,
v being
Vertex of
G2 st
u <> v holds
u,
v are_adjacent
proof
let u2,
v2 be
Vertex of
G2;
( u2 <> v2 implies u2,v2 are_adjacent )
reconsider u1 =
u2,
v1 =
v2 as
Vertex of
G1 by GLIB_006:68;
assume
u2 <> v2
;
u2,v2 are_adjacent
then
u1 <> v1
;
then
u1,
v1 are_adjacent
by A2, CHORD:def 6;
then consider e being
object such that A3:
e Joins u1,
v1,
G1
by CHORD:def 3;
(
u2 <> v &
v2 <> v )
by A1;
then
e Joins u2,
v2,
G2
by A1, A3, Th49;
hence
u2,
v2 are_adjacent
by CHORD:def 3;
verum
end; hence
G2 is
complete
by CHORD:def 6;
V = the_Vertices_of G2
for
x being
object st
x in the_Vertices_of G2 holds
x in V
then
the_Vertices_of G2 c= V
by TARSKI:def 3;
hence
V = the_Vertices_of G2
by A1, XBOOLE_0:def 10;
verum
end;
assume that
A5:
G2 is complete
and
A6:
V = the_Vertices_of G2
; G1 is complete
for u, v being Vertex of G1 st u <> v holds
u,v are_adjacent
proof
let u1,
v1 be
Vertex of
G1;
( u1 <> v1 implies u1,v1 are_adjacent )
assume A7:
u1 <> v1
;
u1,v1 are_adjacent
consider E being
set such that
(
card V = card E &
E misses the_Edges_of G2 &
the_Edges_of G1 = (the_Edges_of G2) \/ E )
and A8:
for
v1 being
object st
v1 in V holds
ex
e1 being
object st
(
e1 in E &
e1 Joins v1,
v,
G1 & ( for
e2 being
object st
e2 Joins v1,
v,
G1 holds
e1 = e2 ) )
by A1, Def4;
A9:
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v}
by A1, Def4;
per cases
( u1 = v or v1 = v or ( u1 <> v & v1 <> v ) )
;
suppose A10:
u1 = v
;
u1,v1 are_adjacent then
v1 <> v
by A7;
then
not
v1 in {v}
by TARSKI:def 1;
then
v1 in the_Vertices_of G2
by A9, XBOOLE_0:def 3;
then consider e1 being
object such that A11:
(
e1 in E &
e1 Joins v1,
v,
G1 )
and
for
e2 being
object st
e2 Joins v1,
v,
G1 holds
e1 = e2
by A6, A8;
e1 Joins u1,
v1,
G1
by A10, A11, GLIB_000:14;
hence
u1,
v1 are_adjacent
by CHORD:def 3;
verum end; suppose A12:
v1 = v
;
u1,v1 are_adjacent then
u1 <> v
by A7;
then
not
u1 in {v}
by TARSKI:def 1;
then
u1 in the_Vertices_of G2
by A9, XBOOLE_0:def 3;
then consider e1 being
object such that A13:
(
e1 in E &
e1 Joins u1,
v,
G1 )
and
for
e2 being
object st
e2 Joins u1,
v,
G1 holds
e1 = e2
by A6, A8;
e1 Joins u1,
v1,
G1
by A12, A13;
hence
u1,
v1 are_adjacent
by CHORD:def 3;
verum end; suppose
(
u1 <> v &
v1 <> v )
;
u1,v1 are_adjacent then
( not
u1 in {v} & not
v1 in {v} )
by TARSKI:def 1;
then reconsider u2 =
u1,
v2 =
v1 as
Vertex of
G2 by A9, XBOOLE_0:def 3;
u2,
v2 are_adjacent
by A5, A7, CHORD:def 6;
then consider e being
object such that A14:
e Joins u2,
v2,
G2
by CHORD:def 3;
e Joins u1,
v1,
G1
by A14, GLIB_006:70;
hence
u1,
v1 are_adjacent
by CHORD:def 3;
verum end; end;
end;
hence
G1 is complete
by CHORD:def 6; verum