for G being SimpleGraph holds union G in union (Mycielskian G)