let G be SimpleGraph; :: thesis: for x, y being set st {[x,(union G)],y} in Edges (Mycielskian G) holds
( x <> y & x in union G & ( y in union G or y = union G ) )
let x, y be set ; :: thesis: ( {[x,(union G)],y} in Edges (Mycielskian G) implies ( x <> y & x in union G & ( y in union G or y = union G ) ) )
assume A: {[x,(union G)],y} in Edges (Mycielskian G) ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )
set uG = union G;
set e = {[x,(union G)],y};

per cases ( {[x,(union G)],y} in Edges G or ex x, y being Element of union G st
( {[x,(union G)],y} = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( {[x,(union G)],y} = {(union G),[y,(union G)]} & y in union G ) ) by A, M0e0;

suppose {[x,(union G)],y} in Edges G ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )

then [x,(union G)] in union G by SG5;
hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by Aux1; :: thesis: verum

end;

suppose ex x, y being Element of union G st
( {[x,(union G)],y} = {x,[y,(union G)]} & {x,y} in Edges G ) ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )

then consider xa, ya being Element of union G such that
A1: {[x,(union G)],y} = {xa,[ya,(union G)]} and
B1: {xa,ya} in Edges G ;
consider xx, yy being set such that
C1: xx <> yy and
D1: ( xx in Vertices G & yy in Vertices G ) and
E1: {xa,ya} = {xx,yy} by B1, SG4;
F1: ( ( xa = xx & ya = yy ) or ( xa = yy & ya = xx ) ) by E1, ZFMISC_1:6;

per cases ( ( xa = [x,(union G)] & y = [ya,(union G)] ) or ( xa = y & [ya,(union G)] = [x,(union G)] ) ) by A1, ZFMISC_1:6;

suppose ( xa = [x,(union G)] & y = [ya,(union G)] ) ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )

hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by D1, Aux1; :: thesis: verum

end;

suppose ( xa = y & [ya,(union G)] = [x,(union G)] ) ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )

hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by C1, D1, F1, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

suppose ex y being Element of union G st
( {[x,(union G)],y} = {(union G),[y,(union G)]} & y in union G ) ; :: thesis: ( x <> y & x in union G & ( y in union G or y = union G ) )

then consider yy being Element of union G such that
A1: {[x,(union G)],y} = {(union G),[yy,(union G)]} and
B1: yy in union G ;
C1: ( ( union G = [x,(union G)] & y = [yy,(union G)] ) or ( union G = y & [x,(union G)] = [yy,(union G)] ) ) by A1, ZFMISC_1:6;
x = yy by C1, Aux2, XTUPLE_0:1;
hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by C1, B1; :: thesis: verum

end;

end;