let G be SimpleGraph; :: thesis: for x, y being set st {[x,(union G)],y} in Mycielskian G holds
x <> y
let x, y be set ; :: thesis: ( {[x,(union G)],y} in Mycielskian G implies x <> y )
set MG = Mycielskian G;
set uG = union G;
assume A: {[x,(union G)],y} in Mycielskian G ; :: thesis: x <> y
assume B: x = y ; :: thesis: contradiction
then [x,(union G)] <> y by Aux3;
then {[x,(union G)],y} in Edges (Mycielskian G) by A, SG4a;
hence contradiction by B, M0e4; :: thesis: verum