let G be SimpleGraph; :: thesis: for L, x being set st x in L & x in Vertices G holds
x in Vertices (G SubgraphInducedBy L)
let L, x be set ; :: thesis: ( x in L & x in Vertices G implies x in Vertices (G SubgraphInducedBy L) )
assume that
A: x in L and
B: x in Vertices G ; :: thesis: x in Vertices (G SubgraphInducedBy L)
C: {x} in G by B, Vertices0;
D: {x} c= L by A, ZFMISC_1:31;
E: {x} in G SubgraphInducedBy L by C, D, XBOOLE_0:def 4;
thus x in Vertices (G SubgraphInducedBy L) by E, Vertices0; :: thesis: verum