set S = { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } ;

now :: thesis: for x being object st x in { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } holds
x in G .allSG()

let x be object ; :: thesis: ( x in { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } implies x in G .allSG() )
assume x in { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } ; :: thesis: x in G .allSG()
then consider V being non empty Subset of (the_Vertices_of G) such that
A1: x = the plain inducedSubgraph of G,V ;
thus x in G .allSG() by A1; :: thesis: verum

end;

hence { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } is Subset of (G .allSG()) by TARSKI:def 3; :: thesis: verum