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

per cases ( {(union G),u} in Edges G or ( ( union G in union G or union G = union G ) & ex y being set st
( y in union G & u = [y,(union G)] ) ) or ( ( u in union G or u = union G ) & ex y being set st
( y in union G & union G = [y,(union G)] ) ) ) by A, M0e1;

suppose {(union G),u} in Edges G ; :: thesis: ex x being set st
( x in union G & u = [x,(union G)] )

then union G in union G by SG5;
hence ex x being set st
( x in union G & u = [x,(union G)] ) ; :: thesis: verum

end;

suppose ( ( union G in union G or union G = union G ) & ex y being set st
( y in union G & u = [y,(union G)] ) ) ; :: thesis: ex x being set st
( x in union G & u = [x,(union G)] )

hence ex x being set st
( x in union G & u = [x,(union G)] ) ; :: thesis: verum

end;

suppose ( ( u in union G or u = union G ) & ex y being set st
( y in union G & union G = [y,(union G)] ) ) ; :: thesis: ex x being set st
( x in union G & u = [x,(union G)] )

then consider y being set such that
y in union G and
A1: union G = [y,(union G)] ;
thus ex x being set st
( x in union G & u = [x,(union G)] ) by A1, Aux2; :: thesis: verum

end;

end;