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