consider T being inducedSubgraph of G,(G .AdjacentSet S);
T is Subgraph of G ;
hence ( S is Subset of (the_Vertices_of G) implies ex b₁ being Subgraph of G st b₁ is inducedSubgraph of G,(G .AdjacentSet S) ) ; :: thesis: verum