let G2 be _Graph; :: thesis: for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let v1, e be object ; :: thesis: for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let v2 be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & not G2 is _trivial implies not G1 is complete )
assume that
A1: ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 ) and
A2: not G2 is _trivial ; :: thesis: not G1 is complete
ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )
proof
consider u1, u2 being Vertex of G2 such that
A3: u1 <> u2 by A2, GLIB_000:21;
A4: ( u1 <> v1 & u2 <> v1 ) by A1;
reconsider u1 = u1, u2 = u2 as Vertex of G1 by Th72;
reconsider v1 = v1 as Vertex of G1 by A1, Th134;
per cases ( u1 <> v2 or u2 <> v2 or ( u1 = v2 & u2 = v2 ) ) ;
suppose A5: u1 <> v2 ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )
take v1 ; :: thesis: ex v being Vertex of G1 st
( v1 <> v & not v1,v are_adjacent )
take u1 ; :: thesis: ( v1 <> u1 & not v1,u1 are_adjacent )
for e1 being object holds not e1 Joins v1,u1,G1 by A1, A5, Th138;
hence ( v1 <> u1 & not v1,u1 are_adjacent ) by A4, CHORD:def 3; :: thesis: verum
end;
suppose A6: u2 <> v2 ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )
take v1 ; :: thesis: ex v being Vertex of G1 st
( v1 <> v & not v1,v are_adjacent )
take u2 ; :: thesis: ( v1 <> u2 & not v1,u2 are_adjacent )
for e1 being object holds not e1 Joins v1,u2,G1 by A1, A6, Th138;
hence ( v1 <> u2 & not v1,u2 are_adjacent ) by A4, CHORD:def 3; :: thesis: verum
end;
suppose ( u1 = v2 & u2 = v2 ) ; :: thesis: ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent )
hence ex u, v being Vertex of G1 st
( u <> v & not u,v are_adjacent ) by A3; :: thesis: verum
end;
end;
end;
hence not G1 is complete by CHORD:def 6; :: thesis: verum