let G, H be SimpleGraph; :: thesis: ( G c= H implies G c= H SubgraphInducedBy (Vertices G) )
assume A: G c= H ; :: thesis: G c= H SubgraphInducedBy (Vertices G)
set L = Vertices G;
let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in G or g in H SubgraphInducedBy (Vertices G) )
assume A1: g in G ; :: thesis: g in H SubgraphInducedBy (Vertices G)
g c= Vertices G by A1, ZFMISC_1:74;
hence g in H SubgraphInducedBy (Vertices G) by A1, A, XBOOLE_0:def 4; :: thesis: verum