let G be SimpleGraph; :: thesis: for x being set st Vertices G = {x} holds
Mycielskian G = {{},{x},{[x,(union G)]},{(union G)},{[x,(union G)],(union G)}}
let a be set ; :: thesis: ( Vertices G = {a} implies Mycielskian G = {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} )
assume A1: Vertices G = {a} ; :: thesis: Mycielskian G = {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}
A2: card (Vertices G) = 1 by A1, CARD_1:30;
A3: a in Vertices G by A1, TARSKI:def 1;
set uG = union G;
set MG = Mycielskian G;
set A = { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
set B = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set C = { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;
consider aa being object such that
A4: union G = {aa} by A2, CARD_2:42;
A5: a = aa by A4, A3, TARSKI:def 1;
A6: [:(union G),{(union G)}:] = {[a,(union G)]} by A4, A5, ZFMISC_1:29;
A7: G is edgeless by A2, Th19;
thus Mycielskian G c= {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} :: according to XBOOLE_0:def 10 :: thesis: {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} c= Mycielskian G

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Mycielskian G or e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} )
assume A8: e in Mycielskian G ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

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 A8, MYCIELSK:4;

suppose e in {{}} ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

then e = {} by TARSKI:def 1;
hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by ENUMSET1:def 3; :: thesis: verum

end;

suppose e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

then consider x being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A9: e = {x} ;
( x in (union G) \/ [:(union G),{(union G)}:] or x in {(union G)} ) by XBOOLE_0:def 3;
then ( x in union G or x in [:(union G),{(union G)}:] or x in {(union G)} ) by XBOOLE_0:def 3;
then ( x = a or x = [a,(union G)] or x = union G ) by A4, A5, A6, TARSKI:def 1;
hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by A9, ENUMSET1:def 3; :: thesis: verum

end;

suppose e in Edges G ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by A7; :: thesis: verum

end;

suppose e in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

then consider x, y being Element of union G such that
e = {x,[y,(union G)]} and
A10: {x,y} in Edges G ;
thus e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by A10, A7; :: thesis: verum

end;

suppose e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ; :: thesis: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}

then consider x being Element of union G such that
A11: e = {(union G),[x,(union G)]} and
x in Vertices G ;
x = a by A4, A5, TARSKI:def 1;
hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by A11, ENUMSET1:def 3; :: thesis: verum

end;

end;

end;

thus {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} c= Mycielskian G :: thesis: verum

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} or e in Mycielskian G )
assume A12: e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} ; :: thesis: e in Mycielskian G

per cases ( e = {} or e = {a} or e = {[a,(union G)]} or e = {(union G)} or e = {[a,(union G)],(union G)} ) by A12, ENUMSET1:def 3;

suppose e = {} ; :: thesis: e in Mycielskian G

hence e in Mycielskian G by Th20; :: thesis: verum

end;

suppose A13: e = {a} ; :: thesis: e in Mycielskian G

a in (union G) \/ [:(union G),{(union G)}:] by A3, XBOOLE_0:def 3;
then a in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } by A13;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

suppose A14: e = {[a,(union G)]} ; :: thesis: e in Mycielskian G

[a,(union G)] in [:(union G),{(union G)}:] by A6, TARSKI:def 1;
then [a,(union G)] in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
then [a,(union G)] in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } by A14;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

suppose A15: e = {(union G)} ; :: thesis: e in Mycielskian G

union G in {(union G)} by TARSKI:def 1;
then union G in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then e in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } by A15;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

suppose e = {[a,(union G)],(union G)} ; :: thesis: e in Mycielskian G

then e in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by A3;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

end;

end;