let G be SimpleGraph; :: thesis: for e being set holds
( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) )
let e be set ; :: thesis: ( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) )
set uG = union G;
set MG = Mycielskian G;
set C = { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;

hereby :: thesis: ( ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) implies e in Edges (Mycielskian G) )

assume A0: e in Edges (Mycielskian G) ; :: thesis: ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )
then consider x, y being set such that
A1: x <> y and
x in Vertices (Mycielskian G) and
y in Vertices (Mycielskian G) and
D1: e = {x,y} by SG4;

per cases ( e in {{}} or e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or e in Edges G or e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) by A0, MYCIELSK:4;

suppose e in {{}} ; :: thesis: ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )

hence ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) by D1, TARSKI:def 1; :: thesis: verum

end;

suppose e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis: ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )

then consider a being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A2: e = {a} and
verum ;
thus ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) by A2, D1, A1, ZFMISC_1:5; :: thesis: verum

end;

suppose ( e in Edges G or e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) ; :: thesis: ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) )

hence ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) ; :: thesis: verum

end;

end;

end;

assume B: ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) ; :: thesis: e in Edges (Mycielskian G)

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

suppose S1: e in Edges G ; :: thesis: e in Edges (Mycielskian G)

A2: card e = 2 by S1, LEdges;
e in Mycielskian G by S1, MYCIELSK:4;
hence e in Edges (Mycielskian G) by A2, LEdges; :: thesis: verum

end;

suppose ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) ; :: thesis: e in Edges (Mycielskian G)

then consider x, y being Element of union G such that
A2: e = {x,[y,(union G)]} and
B2: {x,y} in Edges G ;
C2: e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } by A2, B2;
D2: e in Mycielskian G by C2, MYCIELSK:4;
y in union G by B2, SG5;
then x <> [y,(union G)] by Aux1;
then card e = 2 by A2, CARD_2:57;
hence e in Edges (Mycielskian G) by D2, LEdges; :: thesis: verum

end;

suppose ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ; :: thesis: e in Edges (Mycielskian G)

then consider y being Element of union G such that
A2: e = {(union G),[y,(union G)]} and
B2: y in union G ;
C2: e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by A2, B2;
D2: e in Mycielskian G by C2, MYCIELSK:4;
card e = 2 by Aux2, A2, CARD_2:57;
hence e in Edges (Mycielskian G) by D2, LEdges; :: thesis: verum

end;

end;