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
A1: x in L and
A2: x in Vertices G ; :: thesis: x in Vertices (G SubgraphInducedBy L)
A3: {x} in G by A2, Th24;
A4: {x} c= L by A1, ZFMISC_1:31;
A5: {x} in G SubgraphInducedBy L by A3, A4, XBOOLE_0:def 4;
thus x in Vertices (G SubgraphInducedBy L) by A5, Th24; :: thesis: verum