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 A: x in Vertices (G SubgraphInducedBy L) ; :: thesis: x in L
consider Y being set such that
B: x in Y and
C: Y in G /\ (bool L) by A, TARSKI:def 4;
set y = Y;
Y in bool L by C, XBOOLE_0:def 4;
hence x in L by B; :: thesis: verum