set S = G /\ (bool L);
Aa: {} in G by SG1;
{} c= L by XBOOLE_1:2;
then reconsider S = G /\ (bool L) as non empty set by Aa, XBOOLE_0:def 4;
S is subset-closed by XBOOLE_0:def 4, CLASSES1:def 1, XBOOLE_1:1;
hence G SubgraphInducedBy L is SimpleGraph-like ; :: thesis: verum