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
A: s in Vertices G and
B: t in Vertices G and
C: {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 A, Vertices0; :: thesis: verum

end;

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

then card {s,t} = 2 by CARD_2:57;
then A1: {s,t} in Edges (Mycielskian G) by C, LEdges;

per cases ( {s,t} in Edges G or ( ( s in union G or s = union G ) & ex y being set st
( y in union G & t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) & ex y being set st
( y in union G & s = [y,(union G)] ) ) ) by A1, M0e1;

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 set 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
B1: t = [y,(union G)] ;
thus {s,t} in G by B1, B, Aux1; :: thesis: verum

end;

suppose ( ( t in union G or t = union G ) & ex y being set 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
B1: s = [y,(union G)] ;
thus {s,t} in G by B1, A, Aux1; :: thesis: verum

end;

end;

end;

end;