let G be SimpleGraph; :: thesis: G = G SubgraphInducedBy (Vertices G)
thus G c= G SubgraphInducedBy (Vertices G) :: according to XBOOLE_0:def 10 :: thesis: G SubgraphInducedBy (Vertices G) c= G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in G SubgraphInducedBy (Vertices G) )
assume A1: x in G ; :: thesis: x in G SubgraphInducedBy (Vertices G)
B1: x c= union G by A1, ZFMISC_1:74;
thus x in G SubgraphInducedBy (Vertices G) by A1, B1, XBOOLE_0:def 4; :: thesis: verum

end;

thus G SubgraphInducedBy (Vertices G) c= G ; :: thesis: verum