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 A1: G is void ; :: thesis: size (Mycielskian G) = (3 * (size G)) + (order G)

then A2: Mycielskian G = {{},{(union G)}} by Th88;
A3: size G = 0 by A1, Th17, CARD_1:27;
size (Mycielskian G) = 0

proof

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

end;

hence size (Mycielskian G) = (3 * (size G)) + (order G) by A1, A3; :: 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 Th28;
A7: 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(A7);
then reconsider B = { {(union G),[y,(union G)]} where y is Element of union G : y in union G } as finite set ;
A8: 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 ) } ;
A9: { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } is finite from FRAENKEL:sch 22(A8, A8);
{ {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 object ; :: 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
A10: 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 A10; :: 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 A9;
A11: card B = order G by Th10;
A12: card A = 2 * (size G) by Th15;

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

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

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

suppose a in Edges G ; :: thesis: contradiction

then consider xa, ya being set such that
xa <> ya and
A17: xa in Vertices G and
ya in Vertices G and
A18: a = {xa,ya} by Th11;

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

suppose xa = union G ; :: thesis: contradiction

hence contradiction by A17; :: thesis: verum

end;

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

hence contradiction by A17, Th1; :: thesis: verum

end;

end;

end;

suppose a in A ; :: thesis: contradiction

then consider xa, ya being Element of union G such that
A19: a = {xa,[ya,(union G)]} and
A20: {xa,ya} in Edges G ;
A21: xa in union G by A20, Th13;

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

suppose xa = union G ; :: thesis: contradiction

hence contradiction by A21; :: thesis: verum

end;

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

hence contradiction by A21, Th1; :: thesis: verum

end;

end;

end;

end;

end;

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

assume A meets Edges G ; :: thesis: contradiction
then consider a being object such that
A23: a in A and
A24: a in Edges G by XBOOLE_0:3;
consider xa, ya being Element of union G such that
A25: a = {xa,[ya,(union G)]} and
{xa,ya} in Edges G by A23;
consider xe, ye being set such that
xe <> ye and
A26: xe in Vertices G and
A27: ye in Vertices G and
A28: a = {xe,ye} by A24, Th11;

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

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

hence contradiction by A26, Th1; :: thesis: verum

end;

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

hence contradiction by A27, Th1; :: thesis: verum

end;

end;

end;

thus size (Mycielskian G) = card (((Edges G) \/ A) \/ B) by Th91
.= (card ((Edges G) \/ A)) + (order G) by A11, A13, CARD_2:40
.= ((card (Edges G)) + (2 * (size G))) + (order G) by A12, A22, CARD_2:40
.= (3 * (size G)) + (order G) ; :: thesis: verum

end;

end;