theorem Th99: :: SCMYCIEL:99

for G being SimpleGraph
for x, y being object st {[x,(union G)],y} in Edges (Mycielskian G) holds
( x <> y & x in union G & ( y in union G or y = union G ) )