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 Th84, Th44; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in (Mycielskian G) SubgraphInducedBy (Vertices G) or a in G )
assume A1: a in (Mycielskian G) SubgraphInducedBy (Vertices G) ; :: thesis: a in G
reconsider m = a as set by TARSKI:1;
A2: m in bool (Vertices G) by A1, XBOOLE_0:def 4;
per cases ( m in {{}} or m in { {x} where x is Element of ((Vertices G) \/ [:(Vertices G),{(Vertices G)}:]) \/ {(Vertices G)} : verum } or m in Edges G or m in { {x,[y,(Vertices G)]} where x, y is Element of Vertices G : {x,y} in Edges G } or m in { {(Vertices G),[x,(Vertices G)]} where x is Element of Vertices G : x in Vertices G } ) by A1, MYCIELSK:4;
suppose m 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
A3: m = {x} ;
x in m by A3, TARSKI:def 1;
hence a in G by A2, A3, Th24; :: thesis: verum
end;
suppose m 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
A4: m = {x,[y,(Vertices G)]} and
{x,y} in Edges G ;
[y,(Vertices G)] in m by A4, TARSKI:def 2;
hence a in G by A2, Th1; :: thesis: verum
end;
suppose m 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
A5: m = {(Vertices G),[x,(Vertices G)]} and
x in Vertices G ;
Vertices G in m by A5, TARSKI:def 2;
then Vertices G in Vertices G by A2;
hence a in G ; :: thesis: verum
end;
end;
end;