let G be SimpleGraph; for x, y being set st {[x,(union G)],y} in Mycielskian G holds
x <> y
let x, y be set ; ( {[x,(union G)],y} in Mycielskian G implies x <> y )
set MG = Mycielskian G;
set uG = union G;
assume A1:
{[x,(union G)],y} in Mycielskian G
; x <> y
assume A2:
x = y
; contradiction
then
[x,(union G)] <> y
by Th3;
then
{[x,(union G)],y} in Edges (Mycielskian G)
by A1, Th12;
hence
contradiction
by A2, Th99; verum