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
B: v in g and
C: 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 C, MYCIELSK:4;

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

hence S₁[] by B, 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
A1: g = {h} and
verum ;
B1: ( h in (union G) \/ [:(union G),{(union G)}:] or h in {(union G)} ) by XBOOLE_0:def 3;
C1: v = h by A1, B, TARSKI:def 1;

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

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

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

end;

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

then consider h1, h2 being set such that
A2: h1 in union G and
B2: h2 in {(union G)} and
C2: h = [h1,h2] by ZFMISC_1:def 2;
h2 = union G by B2, TARSKI:def 1;
hence S₁[] by C1, C2, A2; :: thesis: verum

end;

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

hence S₁[] by C1, 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
A1: g1 in Vertices G and
B1: g2 in Vertices G and
C1: g = {g1,g2} by SG4;
thus S₁[] by A1, B1, B, C1, 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
A1: g = {g1,[g2,(union G)]} and
B1: {g1,g2} in Edges G ;
C1: ( g1 in union G & g2 in union G ) by B1, SG5;
( v = g1 or v = [g2,(union G)] ) by A1, B, TARSKI:def 2;
hence S₁[] by C1; :: 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
A1: g = {(union G),[x,(union G)]} and
B1: x in union G ;
( v = union G or v = [x,(union G)] ) by B, A1, TARSKI:def 2;
hence S₁[] by B1; :: thesis: verum

end;

end;

end;

assume A: ( 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)
B: 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 C2: {a} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
B2a: { {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 B2a, C2, 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 A;

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 B; :: 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
A2: x in union G and
B2: v = [x,(union G)] ;
union G in {(union G)} by TARSKI:def 1;
then v in [:(union G),{(union G)}:] by A2, B2, 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 B; :: 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 B; :: thesis: verum

end;

end;