let G be SimpleGraph; :: thesis: Vertices (Mycielskian G) = ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}
set uG = union G;
set MG = Mycielskian G;
set uMG = union (Mycielskian G);
A1: union G in {(union G)} by TARSKI:def 1;
thus union (Mycielskian G) c= ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} :: according to XBOOLE_0:def 10 :: thesis: ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} c= Vertices (Mycielskian G)

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in union (Mycielskian G) or v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} )
assume A2: v in union (Mycielskian G) ; :: thesis: v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}

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 A2, Th85;

suppose v in union G ; :: thesis: v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}

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

end;

suppose ex x being set st
( x in union G & v = [x,(union G)] ) ; :: thesis: v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}

then consider x being set such that
A3: x in union G and
A4: v = [x,(union G)] ;
v in [:(union G),{(union G)}:] by A1, A3, A4, ZFMISC_1:def 2;
then v in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
hence v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose v = union G ; :: thesis: v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}

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

end;

end;

end;

thus ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} c= union (Mycielskian G) :: thesis: verum

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} or v in union (Mycielskian G) )
assume v in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} ; :: thesis: v in union (Mycielskian G)
then A5: ( v in (union G) \/ [:(union G),{(union G)}:] or v in {(union G)} ) by XBOOLE_0:def 3;

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

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

hence v in union (Mycielskian G) by Th85; :: thesis: verum

end;

suppose v in [:(union G),{(union G)}:] ; :: thesis: v in union (Mycielskian G)

then consider x, y being object such that
A6: x in union G and
A7: y in {(union G)} and
A8: v = [x,y] by ZFMISC_1:def 2;
y = union G by A7, TARSKI:def 1;
hence v in union (Mycielskian G) by A6, A8, Th85; :: thesis: verum

end;

suppose v in {(union G)} ; :: thesis: v in union (Mycielskian G)

then v = union G by TARSKI:def 1;
hence v in union (Mycielskian G) by Th85; :: thesis: verum

end;

end;

end;