let G be SimpleGraph; :: thesis: for x, y being object 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 object ; :: 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 A1: {[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 A1, Th90;

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 Th13;
hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by Th1; :: 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
A2: {[x,(union G)],y} = {xa,[ya,(union G)]} and
A3: {xa,ya} in Edges G ;
consider xx, yy being set such that
A4: xx <> yy and
A5: ( xx in Vertices G & yy in Vertices G ) and
A6: {xa,ya} = {xx,yy} by A3, Th11;
A7: ( ( xa = xx & ya = yy ) or ( xa = yy & ya = xx ) ) by A6, ZFMISC_1:6;

per cases ( ( xa = [x,(union G)] & y = [ya,(union G)] ) or ( xa = y & [ya,(union G)] = [x,(union G)] ) ) by A2, 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 A5, Th1; :: 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 A4, A5, A7, 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
A8: {[x,(union G)],y} = {(union G),[yy,(union G)]} and
A9: yy in union G ;
A10: ( ( union G = [x,(union G)] & y = [yy,(union G)] ) or ( union G = y & [x,(union G)] = [yy,(union G)] ) ) by A8, ZFMISC_1:6;
x = yy by A10, Th2, XTUPLE_0:1;
hence ( x <> y & x in union G & ( y in union G or y = union G ) ) by A10, A9; :: thesis: verum

end;

end;