let G be SimpleGraph; :: thesis: G = (Mycielskian G) SubgraphInducedBy (Vertices G)
set L = Vertices G;
set MG = Mycielskian G;
thus G c= (Mycielskian G) SubgraphInducedBy (Vertices G) by M0, Sub0b; :: according to XBOOLE_0:def 10 :: thesis: (Mycielskian G) SubgraphInducedBy (Vertices G) c= G
thus (Mycielskian G) SubgraphInducedBy (Vertices G) c= G :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (Mycielskian G) SubgraphInducedBy (Vertices G) or a in G )
assume Aa: a in (Mycielskian G) SubgraphInducedBy (Vertices G) ; :: thesis: a in G
set m = a;
C1a: a in bool (Vertices G) by Aa, XBOOLE_0:def 4;

per cases ( a in {{}} or a in { {x} where x is Element of ((Vertices G) \/ [:(Vertices G),{(Vertices G)}:]) \/ {(Vertices G)} : verum } or a in Edges G or a in { {x,[y,(Vertices G)]} where x, y is Element of Vertices G : {x,y} in Edges G } or a in { {(Vertices G),[x,(Vertices G)]} where x is Element of Vertices G : x in Vertices G } ) by Aa, MYCIELSK:4;

suppose a in {{}} ; :: thesis: a in G

then a = {} by TARSKI:def 1;
hence a in G by SG1; :: thesis: verum

end;

suppose a in { {x} where x is Element of ((Vertices G) \/ [:(Vertices G),{(Vertices G)}:]) \/ {(Vertices G)} : verum } ; :: thesis: a in G

then consider x being Element of ((Vertices G) \/ [:(Vertices G),{(Vertices G)}:]) \/ {(Vertices G)} such that
A2: a = {x} and
verum ;
x in a by A2, TARSKI:def 1;
hence a in G by C1a, A2, Vertices0; :: thesis: verum

end;

suppose a in Edges G ; :: thesis: a in G

hence a in G ; :: thesis: verum

end;

suppose a in { {x,[y,(Vertices G)]} where x, y is Element of Vertices G : {x,y} in Edges G } ; :: thesis: a in G

then consider x, y being Element of Vertices G such that
A2: a = {x,[y,(Vertices G)]} and
{x,y} in Edges G ;
[y,(Vertices G)] in a by A2, TARSKI:def 2;
hence a in G by C1a, Aux1; :: thesis: verum

end;

suppose a in { {(Vertices G),[x,(Vertices G)]} where x is Element of Vertices G : x in Vertices G } ; :: thesis: a in G

then consider x being Element of Vertices G such that
A2: a = {(Vertices G),[x,(Vertices G)]} and
x in Vertices G ;
Vertices G in a by A2, TARSKI:def 2;
then Vertices G in Vertices G by C1a;
hence a in G ; :: thesis: verum

end;

end;

end;