let G be finite SimpleGraph; :: thesis: order (Mycielskian G) = (2 * (order G)) + 1
set uG = union G;
set MG = Mycielskian G;
B: card [:(union G),{(union G)}:] = order G by CARD_2:6;
C: union G misses [:(union G),{(union G)}:]

proof

assume union G meets [:(union G),{(union G)}:] ; :: thesis: contradiction
then consider a being set such that
A0: a in union G and
B0: a in [:(union G),{(union G)}:] by XBOOLE_0:3;
consider x, y being set such that
x in union G and
B1: y in {(union G)} and
C1: a = [x,y] by B0, ZFMISC_1:def 2;
y = union G by B1, TARSKI:def 1;
hence contradiction by C1, A0, Aux1; :: thesis: verum

end;

D: now :: thesis: not union G in (union G) \/ [:(union G),{(union G)}:]

assume union G in (union G) \/ [:(union G),{(union G)}:] ; :: thesis: contradiction
then ( union G in union G or union G in [:(union G),{(union G)}:] ) by XBOOLE_0:def 3;
then consider x, y being set such that
x in union G and
B1: y in {(union G)} and
C1: union G = [x,y] by ZFMISC_1:def 2;
y = union G by B1, TARSKI:def 1;
hence contradiction by C1, Aux2; :: thesis: verum

end;

thus order (Mycielskian G) = card (((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}) by M0v2
.= (card ((union G) \/ [:(union G),{(union G)}:])) + 1 by D, CARD_2:41
.= ((card (union G)) + (card [:(union G),{(union G)}:])) + 1 by C, CARD_2:40
.= (2 * (order G)) + 1 by B ; :: thesis: verum