let G be SimpleGraph; :: thesis: for u being set st u in Vertices G holds
{[u,(union G)],(union G)} in Mycielskian G
let u be set ; :: thesis: ( u in Vertices G implies {[u,(union G)],(union G)} in Mycielskian G )
assume A1: u in Vertices G ; :: thesis: {[u,(union G)],(union G)} in Mycielskian G
{[u,(union G)],(union G)} in Edges (Mycielskian G) by A1, Th90;
hence {[u,(union G)],(union G)} in Mycielskian G ; :: thesis: verum