let G be SimpleGraph; :: thesis: for s, t being object holds
( not {s,t} in Edges (Mycielskian G) or {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)] ) ) )
let s, t be object ; :: thesis: ( not {s,t} in Edges (Mycielskian G) or {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)] ) ) )
assume A1: {s,t} in Edges (Mycielskian G) ; :: thesis: ( {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)] ) ) )
set uG = union G;

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

suppose {s,t} in Edges G ; :: thesis: ( {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)] ) ) )

hence ( {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)] ) ) ) ; :: thesis: verum

end;

suppose ex x, y being Element of union G st
( {s,t} = {x,[y,(union G)]} & {x,y} in Edges G ) ; :: thesis: ( {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)] ) ) )

then consider x, y being Element of union G such that
A2: {s,t} = {x,[y,(union G)]} and
A3: {x,y} in Edges G ;
A4: ( x in union G & y in union G ) by A3, Th13;
( ( s = x & t = [y,(union G)] ) or ( t = x & s = [y,(union G)] ) ) by A2, ZFMISC_1:6;
hence ( {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; :: thesis: verum

end;

suppose ex y being Element of union G st
( {s,t} = {(union G),[y,(union G)]} & y in union G ) ; :: thesis: ( {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)] ) ) )

then consider y being Element of union G such that
A5: {s,t} = {(union G),[y,(union G)]} and
A6: y in union G ;
( ( s = union G & t = [y,(union G)] ) or ( t = union G & s = [y,(union G)] ) ) by A5, ZFMISC_1:6;
hence ( {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 A6; :: thesis: verum

end;

end;