for G being SimpleGraph
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)] )