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:
A2: now :: thesis: for x being object st x in G2 .AdjacentSet S holds
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 ;
consider v2 being Vertex of G2 such that
A5: v2 in S and
A6: t2,v2 are_adjacent by ;
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;
now :: thesis: for x being object st x in G1 .AdjacentSet S holds
x 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 ;
consider v1 being Vertex of G1 such that
A9: v1 in S and
A10: t1,v1 are_adjacent by ;
reconsider t2 = t1, v2 = v1 as Vertex of G2 by A1;
t2,v2 are_adjacent by ;
hence x in G2 .AdjacentSet S by A8, A9; :: thesis: verum
end;
hence G1 .AdjacentSet S = G2 .AdjacentSet S by ; :: thesis: verum