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