let G be SimpleGraph; :: thesis:
let s, t be set ; :: thesis:
assume that
A1: s in Vertices G and
A2: t in Vertices G and
A3: {s,t} in Mycielskian G ; :: thesis:

per cases ;

suppose s = t ; :: thesis:

then {s,t} = {s} by ENUMSET1:29;
hence {s,t} in G by A1, Th24; :: thesis:

end;

suppose s <> t ; :: thesis:

then card {s,t} = 2 by CARD_2:57;
then A4: {s,t} in Edges (Mycielskian G) by A3, Def1;

per cases in Edges G or ( ( s in union G or s = union G ) & ex y being object st
( y in union G & t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) & ex y being object st
( y in union G & s = [y,(union G)] ) ) ) by A4, Th93;

suppose {s,t} in Edges G ; :: thesis:

hence {s,t} in G ; :: thesis:

end;

suppose ( ( s in union G or s = union G ) & ex y being object st
( y in union G & t = [y,(union G)] ) ) ; :: thesis:

then consider y being set such that
y in union G and
A5: t = [y,(union G)] ;
thus {s,t} in G by A5, A2, Th1; :: thesis:

end;

suppose ( ( t in union G or t = union G ) & ex y being object st
( y in union G & s = [y,(union G)] ) ) ; :: thesis:

then consider y being set such that
y in union G and
A6: s = [y,(union G)] ;
thus {s,t} in G by A6, A1, Th1; :: thesis:

end;

end;

end;

end;