let G be SimpleGraph; :: thesis: for x, y being set holds not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
let x, y be set ; :: thesis: not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
assume A: {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G) ; :: thesis: contradiction
Ab: union G in {x,(union G)} by TARSKI:def 2;
Ac: {x,(union G)} in {{x},{x,(union G)}} by TARSKI:def 2;
B: not [x,(union G)] in union G by Ab, Ac, XREGULAR:7;
C: not [x,(union G)] = union G by Ab, TARSKI:def 2;
Ab1: union G in {y,(union G)} by TARSKI:def 2;
Ac1: {y,(union G)} in {{y},{y,(union G)}} by TARSKI:def 2;
B1: not [y,(union G)] in union G by Ab1, Ac1, XREGULAR:7;
C1: not [y,(union G)] = union G by Ab1, TARSKI:def 2;
{[x,(union G)],[y,(union G)]} in Edges G by A, B, C, B1, C1, M0e1;
hence contradiction by B, SG5; :: thesis: verum