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