let G be SimpleGraph; :: thesis: for x, y being set st x <> y holds
not {[x,(union G)],[y,(union G)]} in Mycielskian G
let x, y be set ; :: thesis: ( x <> y implies not {[x,(union G)],[y,(union G)]} in Mycielskian G )
assume that
A: x <> y and
B: {[x,(union G)],[y,(union G)]} in Mycielskian G ; :: thesis: contradiction
[x,(union G)] <> [y,(union G)] by A, XTUPLE_0:1;
then card {[x,(union G)],[y,(union G)]} = 2 by CARD_2:57;
then {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G) by B, LEdges;
hence contradiction by M0e3; :: thesis: verum