for G1, G2 being _Graph st G1 == G2 holds
for u1 being Vertex of G1
for u2 being Vertex of G2 st u1 = u2 & u1 is simplicial holds
u2 is simplicial