let G be finite SimpleGraph; :: thesis: size (Mycielskian G) = (3 * (size G)) + (order G)
set uG = union G;
set MG = Mycielskian G;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[y,(union G)]} where y is Element of union G : y in union G } ;

per cases ( G is void or not G is void ) ;

suppose S1: G is void ; :: thesis: size (Mycielskian G) = (3 * (size G)) + (order G)

then M1: Mycielskian G = {{},{(union G)}} by MGvoid;
B1: size G = 0 by S1, VoidGE, CARD_1:27;
size (Mycielskian G) = 0

proof

assume not size (Mycielskian G) = 0 ; :: thesis: contradiction
then Edges (Mycielskian G) <> {} ;
then consider e being set such that
A2: e in Edges (Mycielskian G) by XBOOLE_0:def 1;
consider x, y being set such that
B2: x <> y and
( x in Vertices (Mycielskian G) & y in Vertices (Mycielskian G) ) and
C2: e = {x,y} by A2, SG4;
( e = {} or e = {(union G)} ) by M1, A2, TARSKI:def 2;
hence contradiction by C2, B2, ZFMISC_1:5; :: thesis: verum

end;

hence size (Mycielskian G) = (3 * (size G)) + (order G) by S1, B1; :: thesis: verum

end;

suppose not G is void ; :: thesis: size (Mycielskian G) = (3 * (size G)) + (order G)

then reconsider uGf = union G as non empty set by VoidGV;
Ba: uGf is finite ;
deffunc H₁( set ) -> set = {(union G),[$1,(union G)]};
{ H₁(x) where x is Element of uGf : x in uGf } is finite from FRAENKEL:sch 21(Ba);
then reconsider B = { {(union G),[y,(union G)]} where y is Element of union G : y in union G } as finite set ;
Aa: union G is finite ;
deffunc H₂( set , set ) -> set = {$1,[$2,(union G)]};
set AA = { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } ;
Ab: { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } is finite from FRAENKEL:sch 22(Aa, Aa);
{ {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } c= { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or a in { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } )
assume a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: a in { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) }
then consider x, y being Element of union G such that
A1: a = {x,[y,(union G)]} and
{x,y} in Edges G ;
thus a in { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } by A1; :: thesis: verum

end;

then reconsider A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } as finite set by Ab;
B: card B = order G by McopyV;
C: card A = 2 * (size G) by MnewE;

D: now :: thesis: not B meets (Edges G) \/ A

assume B meets (Edges G) \/ A ; :: thesis: contradiction
then consider a being set such that
A1: a in B and
B1: a in (Edges G) \/ A by XBOOLE_0:3;
consider y being Element of union G such that
C1: a = {(union G),[y,(union G)]} and
y in union G by A1;

per cases ( a in Edges G or a in A ) by B1, XBOOLE_0:def 3;

suppose a in Edges G ; :: thesis: contradiction

then consider xa, ya being set such that
xa <> ya and
B2: xa in Vertices G and
ya in Vertices G and
D2: a = {xa,ya} by SG4;

per cases ( xa = union G or xa = [y,(union G)] ) by C1, D2, ZFMISC_1:6;

suppose xa = union G ; :: thesis: contradiction

hence contradiction by B2; :: thesis: verum

end;

suppose xa = [y,(union G)] ; :: thesis: contradiction

hence contradiction by B2, Aux1; :: thesis: verum

end;

end;

end;

suppose a in A ; :: thesis: contradiction

then consider xa, ya being Element of union G such that
A2: a = {xa,[ya,(union G)]} and
B2: {xa,ya} in Edges G ;
C2: xa in union G by B2, SG5;

per cases ( xa = union G or xa = [y,(union G)] ) by C1, A2, ZFMISC_1:6;

suppose xa = union G ; :: thesis: contradiction

hence contradiction by C2; :: thesis: verum

end;

suppose xa = [y,(union G)] ; :: thesis: contradiction

hence contradiction by C2, Aux1; :: thesis: verum

end;

end;

end;

end;

end;

E: now :: thesis: not A meets Edges G

assume A meets Edges G ; :: thesis: contradiction
then consider a being set such that
A1: a in A and
B1: a in Edges G by XBOOLE_0:3;
consider xa, ya being Element of union G such that
A2: a = {xa,[ya,(union G)]} and
{xa,ya} in Edges G by A1;
consider xe, ye being set such that
xe <> ye and
B2a: xe in Vertices G and
C2a: ye in Vertices G and
D2a: a = {xe,ye} by B1, SG4;

per cases ( xe = [ya,(union G)] or ye = [ya,(union G)] ) by A2, D2a, ZFMISC_1:6;

suppose xe = [ya,(union G)] ; :: thesis: contradiction

hence contradiction by B2a, Aux1; :: thesis: verum

end;

suppose ye = [ya,(union G)] ; :: thesis: contradiction

hence contradiction by C2a, Aux1; :: thesis: verum

end;

end;

end;

thus size (Mycielskian G) = card (((Edges G) \/ A) \/ B) by M0e
.= (card ((Edges G) \/ A)) + (order G) by B, D, CARD_2:40
.= ((card (Edges G)) + (2 * (size G))) + (order G) by C, E, CARD_2:40
.= (3 * (size G)) + (order G) ; :: thesis: verum

end;

end;