let G1, G2 be _Graph; for V, E being set
for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds
G3 is inducedSubgraph of G2,V,E
let V, E be set ; for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds
G3 is inducedSubgraph of G2,V,E
let G3 be inducedSubgraph of G1,V,E; ( G1 == G2 implies G3 is inducedSubgraph of G2,V,E )
assume A1:
G1 == G2
; G3 is inducedSubgraph of G2,V,E
hence
G3 is inducedSubgraph of G2,V,E
; verum