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
not
G is
void
;
Mycielskian G is finite then reconsider uGf =
union G as non
empty set by Th28;
A1:
uGf is
finite
;
deffunc H1(
set )
-> set =
{(union G),[G,(union G)]};
A2:
{ H1(x) where x is Element of uGf : x in uGf } is
finite
from FRAENKEL:sch 21(A1);
A3:
union G is
finite
;
deffunc H2(
set ,
set )
-> set =
{G,[c2,(union G)]};
set AA =
{ H2(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) } ;
A4:
{ H2(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= { H2(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or a in { H2(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 }
;
a in { H2(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 { H2(x,y) where x, y is Element of uGf : ( x in union G & y in union G ) }
by A6;
verum
end; deffunc H3(
set )
-> set =
{G};
defpred S1[
set ]
means verum;
{ H3(x) where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : S1[x] } is
finite
from PRE_CIRC:sch 1();
hence
Mycielskian G is
finite
by A2, A4, A5;
verum end;