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 { {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;
end;
end;