defpred S₁[ Nat, set , set ] means ( ( $2 is SimpleGraph implies ex G being SimpleGraph st
( $2 = G & $3 = Mycielskian G ) ) & ( $2 is not SimpleGraph implies $3 = $2 ) );
P: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]

per cases ( x is SimpleGraph or not x is SimpleGraph ) ;

suppose x is SimpleGraph ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider G = x as SimpleGraph ;
Mycielskian G = Mycielskian G ;
hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

suppose x is not SimpleGraph ; :: thesis: ex y being set st S₁[n,x,y]

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

end;

end;

consider f being Function such that
A: dom f = NAT and
B: f . 0 = G and
C: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(P);
reconsider f = f as NAT -defined Function by A, RELAT_1:def 18;
reconsider f = f as ManySortedSet of NAT by A, PARTFUN1:def 2;
take f ; :: thesis: ex myc being Function st
( f = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) )
take myc = f; :: thesis: ( f = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) )
thus f = myc ; :: thesis: ( myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) )
thus myc . 0 = G by B; :: thesis: for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G
let k be Nat; :: thesis: for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G
let G be SimpleGraph; :: thesis: ( G = myc . k implies myc . (k + 1) = Mycielskian G )
assume Z: G = myc . k ; :: thesis: myc . (k + 1) = Mycielskian G
k in NAT by ORDINAL1:def 12;
then ex G being SimpleGraph st
( f . k = G & f . (k + 1) = Mycielskian G ) by C, Z;
hence myc . (k + 1) = Mycielskian G by Z; :: thesis: verum