let G1, G2 be _Graph; :: thesis:
assume A1: G1 == G2 ; :: thesis:
let S be set ; :: thesis:

let x be object ; :: thesis:
assume A3: x in G2 .AdjacentSet S ; :: thesis:
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:

end;

let x be object ; :: thesis:
assume A7: x in G1 .AdjacentSet S ; :: thesis:
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:

end;