let G be void SimpleGraph; :: thesis: Mycielskian G = {{},{(union G)}}
set uG = union G;
A1: { {(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 object such that
A2: 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
A3: x in Vertices G by A2;
thus contradiction by A3; :: thesis: verum

end;

A4: { {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 object such that
A5: 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
A6: {x,y} in Edges G by A5;
thus contradiction by A6, Th13; :: thesis: verum

end;

A7: Edges G = {}

proof

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

end;

A10: { {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 object ; :: 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
A11: a = {x} ;
x = union G by TARSKI:def 1;
hence a in {{(union G)}} by A11, 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 object ; :: 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 A12: 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 A12; :: thesis: verum

end;

end;

thus Mycielskian G = {{},{(union G)}} by A1, A4, A7, A10, ENUMSET1:1; :: thesis: verum