let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies for S being set holds G1 .AdjacentSet S = G2 .AdjacentSet S )
assume A1:
G1 == G2
; :: thesis: for S being set holds G1 .AdjacentSet S = G2 .AdjacentSet S
let S be set ; :: thesis: G1 .AdjacentSet S = G2 .AdjacentSet S
A2:
now let x be
set ;
:: thesis: ( x in G1 .AdjacentSet S implies x in G2 .AdjacentSet S )assume A3:
x in G1 .AdjacentSet S
;
:: thesis: x in G2 .AdjacentSet Sreconsider t1 =
x as
Vertex of
G1 by A3;
A4:
( not
t1 in S & ex
v being
Vertex of
G1 st
(
v in S &
t1,
v are_adjacent ) )
by A3, Th50;
consider v1 being
Vertex of
G1 such that A5:
(
v1 in S &
t1,
v1 are_adjacent )
by A3, Th50;
reconsider t2 =
t1,
v2 =
v1 as
Vertex of
G2 by A1, GLIB_000:def 36;
t2,
v2 are_adjacent
by A1, A5, Th44;
hence
x in G2 .AdjacentSet S
by A4, A5;
:: thesis: verum end;
now let x be
set ;
:: thesis: ( x in G2 .AdjacentSet S implies x in G1 .AdjacentSet S )assume A6:
x in G2 .AdjacentSet S
;
:: thesis: x in G1 .AdjacentSet Sreconsider t2 =
x as
Vertex of
G2 by A6;
A7:
( not
t2 in S & ex
v being
Vertex of
G2 st
(
v in S &
t2,
v are_adjacent ) )
by A6, Th50;
consider v2 being
Vertex of
G2 such that A8:
(
v2 in S &
t2,
v2 are_adjacent )
by A6, Th50;
reconsider t1 =
t2,
v1 =
v2 as
Vertex of
G1 by A1, GLIB_000:def 36;
t1,
v1 are_adjacent
by A1, A8, Th44;
hence
x in G1 .AdjacentSet S
by A7, A8;
:: thesis: verum end;
hence
G1 .AdjacentSet S = G2 .AdjacentSet S
by A2, TARSKI:2; :: thesis: verum