:: deftheorem defines Mycielskian SCMYCIEL:def 25 :
for G being SimpleGraph holds Mycielskian G = ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;