let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds
for v being Vertex of H st u = v holds
G .AdjacentSet {u} = H .AdjacentSet {v}
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds
for v being Vertex of H st u = v holds
G .AdjacentSet {u} = H .AdjacentSet {v}
let G2 be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds
for v being Vertex of G2 st u = v holds
G .AdjacentSet {u} = G2 .AdjacentSet {v}
let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S implies for v being Vertex of G2 st u = v holds
G .AdjacentSet {u} = G2 .AdjacentSet {v} )
assume A1:
( u in S & G .AdjacentSet {u} c= S )
; :: thesis: for v being Vertex of G2 st u = v holds
G .AdjacentSet {u} = G2 .AdjacentSet {v}
let v be Vertex of G2; :: thesis: ( u = v implies G .AdjacentSet {u} = G2 .AdjacentSet {v} )
assume A2:
u = v
; :: thesis: G .AdjacentSet {u} = G2 .AdjacentSet {v}
now let x be
set ;
:: thesis: ( ( x in G .AdjacentSet {u} implies x in G2 .AdjacentSet {v} ) & ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} ) )hereby :: thesis: ( x in G2 .AdjacentSet {v} implies x in G .AdjacentSet {u} )
assume A3:
x in G .AdjacentSet {u}
;
:: thesis: x in G2 .AdjacentSet {v}then reconsider y =
x as
Vertex of
G ;
reconsider w =
x as
Vertex of
G2 by A1, A3, GLIB_000:def 39;
(
y <> u &
y,
u are_adjacent )
by A3, Th52;
then consider e being
set such that A4:
e Joins y,
u,
G
by Def3;
e Joins y,
u,
G2
by A1, A3, A4, Th19;
then
(
w <> v &
w,
v are_adjacent )
by A2, A3, Def3, Th52;
hence
x in G2 .AdjacentSet {v}
by Th52;
:: thesis: verum
end; assume A5:
x in G2 .AdjacentSet {v}
;
:: thesis: x in G .AdjacentSet {u}then reconsider y =
x as
Vertex of
G2 ;
x in the_Vertices_of G2
by A5;
then reconsider w =
x as
Vertex of
G ;
(
y <> v &
y,
v are_adjacent )
by A5, Th52;
then consider e being
set such that A6:
e Joins y,
v,
G2
by Def3;
e Joins y,
v,
G
by A6, GLIB_000:75;
then
(
w <> u &
w,
u are_adjacent )
by A2, A5, Def3, Th52;
hence
x in G .AdjacentSet {u}
by Th52;
:: thesis: verum end;
hence
G .AdjacentSet {u} = G2 .AdjacentSet {v}
by TARSKI:2; :: thesis: verum