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

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 :: thesis: for x being object st x in G2 .AdjacentSet S holds

x in G1 .AdjacentSet S

x in G1 .AdjacentSet S

let x be object ; :: thesis: ( x in G2 .AdjacentSet S implies x in G1 .AdjacentSet S )

assume A3: x in G2 .AdjacentSet S ; :: thesis: x in G1 .AdjacentSet S

reconsider t2 = x as Vertex of G2 by A3;

A4: not t2 in S by A3, Th49;

consider v2 being Vertex of G2 such that

A5: v2 in S and

A6: t2,v2 are_adjacent by A3, Th49;

reconsider t1 = t2, v1 = v2 as Vertex of G1 by A1;

t1,v1 are_adjacent by A1, A6, Th43;

hence x in G1 .AdjacentSet S by A4, A5; :: thesis: verum

end;assume A3: x in G2 .AdjacentSet S ; :: thesis: x in G1 .AdjacentSet S

reconsider t2 = x as Vertex of G2 by A3;

A4: not t2 in S by A3, Th49;

consider v2 being Vertex of G2 such that

A5: v2 in S and

A6: t2,v2 are_adjacent by A3, Th49;

reconsider t1 = t2, v1 = v2 as Vertex of G1 by A1;

t1,v1 are_adjacent by A1, A6, Th43;

hence x in G1 .AdjacentSet S by A4, A5; :: thesis: verum

now :: thesis: for x being object st x in G1 .AdjacentSet S holds

x in G2 .AdjacentSet S

hence
G1 .AdjacentSet S = G2 .AdjacentSet S
by A2, TARSKI:2; :: thesis: verumx in G2 .AdjacentSet S

let x be object ; :: thesis: ( x in G1 .AdjacentSet S implies x in G2 .AdjacentSet S )

assume A7: x in G1 .AdjacentSet S ; :: thesis: x in G2 .AdjacentSet S

reconsider t1 = x as Vertex of G1 by A7;

A8: not t1 in S by A7, Th49;

consider v1 being Vertex of G1 such that

A9: v1 in S and

A10: t1,v1 are_adjacent by A7, Th49;

reconsider t2 = t1, v2 = v1 as Vertex of G2 by A1;

t2,v2 are_adjacent by A1, A10, Th43;

hence x in G2 .AdjacentSet S by A8, A9; :: thesis: verum

end;assume A7: x in G1 .AdjacentSet S ; :: thesis: x in G2 .AdjacentSet S

reconsider t1 = x as Vertex of G1 by A7;

A8: not t1 in S by A7, Th49;

consider v1 being Vertex of G1 such that

A9: v1 in S and

A10: t1,v1 are_adjacent by A7, Th49;

reconsider t2 = t1, v2 = v1 as Vertex of G2 by A1;

t2,v2 are_adjacent by A1, A10, Th43;

hence x in G2 .AdjacentSet S by A8, A9; :: thesis: verum