let G be SimpleGraph; :: thesis: for x, y being set st {x,y} in Edges G holds
{[x,(union G)],y} in Mycielskian G
set uG = union G;
let x, y be set ; :: thesis: ( {x,y} in Edges G implies {[x,(union G)],y} in Mycielskian G )
A1: { {xx,[yy,(union G)]} where xx, yy is Element of union G : {xx,yy} in Edges G } c= Mycielskian G by MYCIELSK:3;
assume A2: {x,y} in Edges G ; :: thesis: {[x,(union G)],y} in Mycielskian G
then ( x in union G & y in union G ) by Th13;
then {[x,(union G)],y} in { {xx,[yy,(union G)]} where xx, yy is Element of union G : {xx,yy} in Edges G } by A2;
hence {[x,(union G)],y} in Mycielskian G by A1; :: thesis: verum