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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in G SubgraphInducedBy (Vertices G) )
reconsider xx = x as set by TARSKI:1;
assume A1: x in G ; :: thesis: x in G SubgraphInducedBy (Vertices G)
A2: xx c= union G by A1, ZFMISC_1:74;
thus x in G SubgraphInducedBy (Vertices G) by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

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