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 Aa: Vertices G = {a} ; :: thesis: Mycielskian G = {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}}
A: card (Vertices G) = 1 by Aa, CARD_1:30;
B: a in Vertices G by Aa, 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 set such that
Ca: union G = {aa} by A, CARD_2:42;
C: a = aa by Ca, B, TARSKI:def 1;
D: [:(union G),{(union G)}:] = {[a,(union G)]} by Ca, C, ZFMISC_1:29;
E0: G is edgeless by A, GsingleE;
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 set ; :: 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 A1: 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 A1, 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
B1: e = {x} and
verum ;
( 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 Ca, C, D, TARSKI:def 1;
hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by B1, 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 E0, Ledgeless; :: 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
B1: {x,y} in Edges G ;
thus e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by B1, E0, Ledgeless; :: 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
A1: e = {(union G),[x,(union G)]} and
x in Vertices G ;
x = a by Ca, C, TARSKI:def 1;
hence e in {{},{a},{[a,(union G)]},{(union G)},{[a,(union G)],(union G)}} by A1, 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 set ; :: 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 A1: 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 A1, ENUMSET1:def 3;

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

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

end;

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

a in (union G) \/ [:(union G),{(union G)}:] by B, 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 S1;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

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

[a,(union G)] in [:(union G),{(union G)}:] by D, 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 S1;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

suppose S1: 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 S1;
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 B;
hence e in Mycielskian G by MYCIELSK:4; :: thesis: verum

end;

end;

end;