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 A1: {[x,(union G)],y} in Mycielskian G ; :: thesis: x <> y
assume A2: x = y ; :: thesis: 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; :: thesis: verum