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