let G1 be _Graph; for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
let G2 be removeParallelEdges of G1; for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
let v1 be Vertex of G1; for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
let v2 be Vertex of G2; ( v1 = v2 implies ( v1 is isolated iff v2 is isolated ) )
assume A1:
v1 = v2
; ( v1 is isolated iff v2 is isolated )
hence
( v1 is isolated implies v2 is isolated )
by GLIB_000:83; ( v2 is isolated implies v1 is isolated )
assume
v2 is isolated
; v1 is isolated
then A2:
v2 .edgesInOut() = {}
by GLIB_000:def 49;
v1 .edgesInOut() = {}
proof
assume
v1 .edgesInOut() <> {}
;
contradiction
then consider e0 being
object such that A3:
e0 in v1 .edgesInOut()
by XBOOLE_0:def 1;
consider w being
Vertex of
G1 such that A4:
e0 Joins v1,
w,
G1
by A3, GLIB_000:64;
consider E1 being
RepEdgeSelection of
G1 such that A5:
G2 is
inducedSubgraph of
G1,
the_Vertices_of G1,
E1
by Def7;
consider e1 being
object such that A6:
(
e1 Joins v1,
w,
G1 &
e1 in E1 )
and
for
e9 being
object st
e9 Joins v1,
w,
G1 &
e9 in E1 holds
e9 = e1
by A4, Def5;
(
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) )
by GLIB_000:34;
then A7:
(
the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G2 = E1 )
by A5, GLIB_000:def 37;
then reconsider w =
w as
Vertex of
G2 ;
A8:
e1 Joins v2,
w,
G2
by A1, A6, A7, GLIB_000:73;
e1 is
set
by TARSKI:1;
hence
contradiction
by A2, A8, GLIB_000:64;
verum
end;
hence
v1 is isolated
by GLIB_000:def 49; verum