let G be finite SimpleGraph; :: thesis: order (Mycielskian G) = (2 * (order G)) + 1
set uG = union G;
set MG = Mycielskian G;
A1: card [:(union G),{(union G)}:] = order G by CARD_1:69;
A2: union G misses [:(union G),{(union G)}:]

proof

assume union G meets [:(union G),{(union G)}:] ; :: thesis: contradiction
then consider a being object such that
A3: a in union G and
A4: a in [:(union G),{(union G)}:] by XBOOLE_0:3;
consider x, y being object such that
x in union G and
A5: y in {(union G)} and
A6: a = [x,y] by A4, ZFMISC_1:def 2;
y = union G by A5, TARSKI:def 1;
hence contradiction by A6, A3, Th1; :: thesis: verum

end;

A7: 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 object such that
x in union G and
A8: y in {(union G)} and
A9: union G = [x,y] by ZFMISC_1:def 2;
y = union G by A8, TARSKI:def 1;
hence contradiction by A9, Th2; :: thesis: verum

end;

thus order (Mycielskian G) = card (((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}) by Th86
.= (card ((union G) \/ [:(union G),{(union G)}:])) + 1 by A7, CARD_2:41
.= ((card (union G)) + (card [:(union G),{(union G)}:])) + 1 by A2, CARD_2:40
.= (2 * (order G)) + 1 by A1 ; :: thesis: verum