let G be SimpleGraph; :: thesis: union G in union (Mycielskian G)
union G in {(union G)} by TARSKI:def 1;
then union G in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
hence union G in union (Mycielskian G) by M0v2; :: thesis: verum