let G be SimpleGraph; :: thesis: G c= Mycielskian G
set MG = Mycielskian G;
set uG = union G;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in Mycielskian G )
assume x in G ; :: thesis: x in Mycielskian G
then x in ({{}} \/ (singletons (union G))) \/ (Edges G) by Th27;
then A1: ( x in {{}} \/ (singletons (union G)) or x in Edges G ) by XBOOLE_0:def 3;
per cases ( x in {{}} or x in singletons (union G) or x in Edges G ) by A1, XBOOLE_0:def 3;
suppose x in {{}} ; :: thesis: x in Mycielskian G
then x = {} by TARSKI:def 1;
hence x in Mycielskian G by Th20; :: thesis: verum
end;
suppose x in singletons (union G) ; :: thesis: x in Mycielskian G
then consider f being Subset of (union G) such that
A2: x = f and
A3: f is 1 -element ;
consider a being set such that
A4: a in union G and
A5: f = {a} by A3, Th9;
a in (union G) \/ [:(union G),{(union G)}:] by A4, XBOOLE_0:def 3;
then a in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then x in { {xx} where xx is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } by A2, A5;
hence x in Mycielskian G by MYCIELSK:4; :: thesis: verum
end;
suppose A6: x in Edges G ; :: thesis: x in Mycielskian G
Edges G c= Mycielskian G by MYCIELSK:3;
hence x in Mycielskian G by A6; :: thesis: verum
end;
end;