let G be SimpleGraph; :: thesis: for L, x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
let L be set ; :: thesis: for x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
set S = G /\ (bool L);
let x be set ; :: thesis: ( x in Vertices (G SubgraphInducedBy L) implies x in L )
assume A1: x in Vertices (G SubgraphInducedBy L) ; :: thesis: x in L
consider Y being set such that
A2: x in Y and
A3: Y in G /\ (bool L) by A1, TARSKI:def 4;
set y = Y;
Y in bool L by A3, XBOOLE_0:def 4;
hence x in L by A2; :: thesis: verum