let G be void SimpleGraph; :: thesis: Mycielskian G = {{},{(union G)}}
set uG = union G;
A: { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } = {}

proof

assume not { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } = {} ; :: thesis: contradiction
then consider e being set such that
A1: e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by XBOOLE_0:def 1;
consider x being Element of union G such that
e = {(union G),[x,(union G)]} and
B1: x in Vertices G by A1;
thus contradiction by B1; :: thesis: verum

end;

B: { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } = {}

proof

assume not { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } = {} ; :: thesis: contradiction
then consider e being set such that
A1: e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } by XBOOLE_0:def 1;
consider x, y being Element of union G such that
e = {x,[y,(union G)]} and
B1: {x,y} in Edges G by A1;
thus contradiction by B1, SG5; :: thesis: verum

end;

C: Edges G = {}

proof

assume not Edges G = {} ; :: thesis: contradiction
then consider e being set such that
A1: e in Edges G by XBOOLE_0:def 1;
consider x, y being set such that
x <> y and
B1: x in Vertices G and
( y in Vertices G & e = {x,y} ) by A1, SG4;
thus contradiction by B1; :: thesis: verum

end;

D: { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } = {{(union G)}}

proof

thus { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } c= {{(union G)}} :: according to XBOOLE_0:def 10 :: thesis: {{(union G)}} c= { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or a in {{(union G)}} )
assume a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis: a in {{(union G)}}
then consider x being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A1: a = {x} and
verum ;
x = union G by TARSKI:def 1;
hence a in {{(union G)}} by A1, TARSKI:def 1; :: thesis: verum

end;

thus {{(union G)}} c= { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {{(union G)}} or a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } )
assume a in {{(union G)}} ; :: thesis: a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum }
then A1: a = {(union G)} by TARSKI:def 1;
union G in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by TARSKI:def 1;
hence a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } by A1; :: thesis: verum

end;

end;

thus Mycielskian G = {{},{(union G)}} by A, B, C, D, ENUMSET1:1; :: thesis: verum