for G being SimpleGraph
for s, t being object holds
( not {s,t} in Edges (Mycielskian G) or {s,t} in Edges G or ( ( s in union G or s = union G ) & ex y being object st
( y in union G & t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) & ex y being object st
( y in union G & s = [y,(union G)] ) ) )