let G be SimpleGraph; :: thesis: for x, y being set st x in Vertices G & y in Vertices G & {x,y} in Mycielskian G holds
{x,y} in G
let s, t be set ; :: thesis: ( s in Vertices G & t in Vertices G & {s,t} in Mycielskian G implies {s,t} in G )
assume that
A1: s in Vertices G and
A2: t in Vertices G and
A3: {s,t} in Mycielskian G ; :: thesis: {s,t} in G

per cases ( s = t or s <> t ) ;

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

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

end;

suppose s <> t ; :: thesis: {s,t} in G

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

per cases ( {s,t} 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: {s,t} in G

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

end;

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

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: verum

end;

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

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: verum

end;

end;

end;

end;