set uG = union G;
set MG = Mycielskian G;
set C = { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;

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

suppose G is void ; :: thesis: Mycielskian G is finite

then Mycielskian G = {{},{(union G)}} by Th88;
hence Mycielskian G is finite ; :: thesis: verum

end;

suppose not G is void ; :: thesis: Mycielskian G is finite

then reconsider uGf = union G as non empty set by Th28;
A1: uGf is finite ;
deffunc H₁( set ) -> set = {(union G),[G,(union G)]};
A2: { H₁(x) where x is Element of uGf : x in uGf } is finite from FRAENKEL:sch 21(A1);
A3: union G is finite ;
deffunc H₂( set , set ) -> set = {G,[c₂,(union G)]};
set AA = { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } ;
A4: { H₂(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } is finite from FRAENKEL:sch 22(A3, A3);
A5: { {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
A6: 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 A6; :: thesis: verum

end;

deffunc H₃( set ) -> set = {G};
defpred S₁[ set ] means verum;
{ H₃(x) where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : S₁[x] } is finite from PRE_CIRC:sch 1();
hence Mycielskian G is finite by A2, A4, A5; :: thesis: verum

end;

end;