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 Th86; :: thesis: verum