let G be SimpleGraph; :: thesis: for v being set holds
( v in Vertices (Mycielskian G) iff ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) )
let v be set ; :: thesis: ( v in Vertices (Mycielskian G) iff ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) )
set uG = union G;
set MG = Mycielskian G;
set uMG = union (Mycielskian G);

hereby :: thesis: ( ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) implies v in Vertices (Mycielskian G) )

assume v in Vertices (Mycielskian G) ; :: thesis: S₁[]
then consider g being set such that
A1: v in g and
A2: g in Mycielskian G by TARSKI:def 4;
defpred S₁[] means ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G );

per cases ( g in {{}} or g in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or g in Edges G or g in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or g in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) by A2, MYCIELSK:4;

suppose g in {{}} ; :: thesis: S₁[]

hence S₁[] by A1, TARSKI:def 1; :: thesis: verum

end;

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

then consider h being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A3: g = {h} ;
A4: ( h in (union G) \/ [:(union G),{(union G)}:] or h in {(union G)} ) by XBOOLE_0:def 3;
A5: v = h by A3, A1, TARSKI:def 1;

per cases ( h in union G or h in [:(union G),{(union G)}:] or h in {(union G)} ) by A4, XBOOLE_0:def 3;

suppose h in union G ; :: thesis: S₁[]

hence S₁[] by A3, A1, TARSKI:def 1; :: thesis: verum

end;

suppose h in [:(union G),{(union G)}:] ; :: thesis: S₁[]

then consider h1, h2 being object such that
A6: h1 in union G and
A7: h2 in {(union G)} and
A8: h = [h1,h2] by ZFMISC_1:def 2;
h2 = union G by A7, TARSKI:def 1;
hence S₁[] by A5, A8, A6; :: thesis: verum

end;

suppose h in {(union G)} ; :: thesis: S₁[]

hence S₁[] by A5, TARSKI:def 1; :: thesis: verum

end;

end;

end;

suppose g in Edges G ; :: thesis: S₁[]

then consider g1, g2 being set such that
g1 <> g2 and
A9: g1 in Vertices G and
A10: g2 in Vertices G and
A11: g = {g1,g2} by Th11;
thus S₁[] by A9, A10, A1, A11, TARSKI:def 2; :: thesis: verum

end;

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

then consider g1, g2 being Element of union G such that
A12: g = {g1,[g2,(union G)]} and
A13: {g1,g2} in Edges G ;
A14: ( g1 in union G & g2 in union G ) by A13, Th13;
( v = g1 or v = [g2,(union G)] ) by A12, A1, TARSKI:def 2;
hence S₁[] by A14; :: thesis: verum

end;

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

then consider x being Element of union G such that
A15: g = {(union G),[x,(union G)]} and
A16: x in union G ;
( v = union G or v = [x,(union G)] ) by A1, A15, TARSKI:def 2;
hence S₁[] by A16; :: thesis: verum

end;

end;

end;

assume A17: ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) ; :: thesis: v in Vertices (Mycielskian G)
A18: for a being set st a in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} holds
a in union (Mycielskian G)

proof

let a be set ; :: thesis: ( a in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} implies a in union (Mycielskian G) )
assume a in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} ; :: thesis: a in union (Mycielskian G)
then A19: {a} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
A20: { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } c= Mycielskian G by MYCIELSK:3;
a in {a} by TARSKI:def 1;
hence a in union (Mycielskian G) by A20, A19, TARSKI:def 4; :: thesis: verum

end;

per cases ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) by A17;

suppose v in union G ; :: thesis: v in Vertices (Mycielskian G)

then v in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
then v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
hence v in Vertices (Mycielskian G) by A18; :: thesis: verum

end;

suppose ex x being set st
( x in union G & v = [x,(union G)] ) ; :: thesis: v in Vertices (Mycielskian G)

then consider x being set such that
A21: x in union G and
A22: v = [x,(union G)] ;
union G in {(union G)} by TARSKI:def 1;
then v in [:(union G),{(union G)}:] by A21, A22, ZFMISC_1:def 2;
then v in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
then v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
hence v in Vertices (Mycielskian G) by A18; :: thesis: verum

end;

suppose v = union G ; :: thesis: v in Vertices (Mycielskian G)

then v in {(union G)} by TARSKI:def 1;
then v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
hence v in Vertices (Mycielskian G) by A18; :: thesis: verum

end;

end;