let G be SimpleGraph; :: thesis: for u being object st {(union G),u} in Edges (Mycielskian G) holds
ex x being object st
( x in union G & u = [x,(union G)] )
let u be object ; :: thesis: ( {(union G),u} in Edges (Mycielskian G) implies ex x being object st
( x in union G & u = [x,(union G)] ) )
assume A1: {(union G),u} in Edges (Mycielskian G) ; :: thesis: ex x being object 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 object st
( y in union G & u = [y,(union G)] ) ) or ( ( u in union G or u = union G ) & ex y being object st
( y in union G & union G = [y,(union G)] ) ) ) by A1, Th93;

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

then union G in union G by Th13;
hence ex x being object 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 object st
( y in union G & u = [y,(union G)] ) ) ; :: thesis: ex x being object st
( x in union G & u = [x,(union G)] )

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

end;

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

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

end;

end;