let G be SimpleGraph; :: thesis: for x, y being set st y in union G & {[x,(union G)],y} in Mycielskian G holds
{x,y} in G
set MG = Mycielskian G;
set uG = union G;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ;
let x, y be set ; :: thesis: ( y in union G & {[x,(union G)],y} in Mycielskian G implies {x,y} in G )
assume A0: y in union G ; :: thesis: ( not {[x,(union G)],y} in Mycielskian G or {x,y} in G )
assume {[x,(union G)],y} in Mycielskian G ; :: thesis: {x,y} in G
then {[x,(union G)],y} in ({{}} \/ (singletons (Vertices (Mycielskian G)))) \/ (Edges (Mycielskian G)) by SG0;
then A: ( {[x,(union G)],y} in {{}} \/ (singletons (Vertices (Mycielskian G))) or {[x,(union G)],y} in Edges (Mycielskian G) ) by XBOOLE_0:def 3;

per cases ( {[x,(union G)],y} in {{}} or {[x,(union G)],y} in singletons (Vertices (Mycielskian G)) or {[x,(union G)],y} in Edges (Mycielskian G) ) by A, XBOOLE_0:def 3;

suppose {[x,(union G)],y} in {{}} ; :: thesis: {x,y} in G

hence {x,y} in G by TARSKI:def 1; :: thesis: verum

end;

suppose {[x,(union G)],y} in singletons (Vertices (Mycielskian G)) ; :: thesis: {x,y} in G

then consider f being Subset of (Vertices (Mycielskian G)) such that
A1: f = {[x,(union G)],y} and
B1: f is 1 -element ;
consider s being set such that
s in Vertices (Mycielskian G) and
D1: f = {s} by B1, BSPACEdef9;
E1: card f = 1 by D1, CARD_1:30;
y = [x,(union G)] by E1, A1, CARD_2:57;
hence {x,y} in G by A0, Aux1; :: thesis: verum

end;

suppose {[x,(union G)],y} in Edges (Mycielskian G) ; :: thesis: {x,y} in G

then {[x,(union G)],y} in ((Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[y,(union G)]} where y is Element of union G : y in union G } by M0e;
then A2: ( {[x,(union G)],y} in (Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or {[x,(union G)],y} in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ) by XBOOLE_0:def 3;

per cases ( {[x,(union G)],y} in Edges G or {[x,(union G)],y} in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or {[x,(union G)],y} in { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ) by A2, XBOOLE_0:def 3;

suppose {[x,(union G)],y} in Edges G ; :: thesis: {x,y} in G

then [x,(union G)] in union G by SG5;
hence {x,y} in G by Aux1; :: thesis: verum

end;

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

then consider xx, yy being Element of union G such that
A3: {[x,(union G)],y} = {xx,[yy,(union G)]} and
B3: {xx,yy} in Edges G ;
C3: ( xx in union G & yy in union G ) by B3, SG5;
( ( [x,(union G)] = xx & y = [yy,(union G)] ) or ( [x,(union G)] = [yy,(union G)] & y = xx ) ) by A3, ZFMISC_1:6;
then ( x = yy & y = xx ) by XTUPLE_0:1, C3, Aux1;
hence {x,y} in G by B3; :: thesis: verum

end;

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

then consider yy being Element of union G such that
A3: {[x,(union G)],y} = {(union G),[yy,(union G)]} and
yy in union G ;
( ( [x,(union G)] = union G & y = [yy,(union G)] ) or ( [x,(union G)] = [yy,(union G)] & y = union G ) ) by A3, ZFMISC_1:6;
hence {x,y} in G by Aux1, A0; :: thesis: verum

end;

end;

end;

end;