let G be SimpleGraph; :: thesis: for x, y being object holds not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
let x, y be object ; :: thesis: not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
assume A1: {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G) ; :: thesis: contradiction
A2: union G in {x,(union G)} by TARSKI:def 2;
A3: {x,(union G)} in {{x},{x,(union G)}} by TARSKI:def 2;
A4: not [x,(union G)] in union G by A2, A3, XREGULAR:7;
A5: not [x,(union G)] = union G by A2, TARSKI:def 2;
A6: union G in {y,(union G)} by TARSKI:def 2;
A7: {y,(union G)} in {{y},{y,(union G)}} by TARSKI:def 2;
A8: not [y,(union G)] in union G by A6, A7, XREGULAR:7;
A9: not [y,(union G)] = union G by A6, TARSKI:def 2;
{[x,(union G)],[y,(union G)]} in Edges G by A1, A4, A5, A8, A9, Th93;
hence contradiction by A4, Th13; :: thesis: verum