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 ) );
A1: for n being Nat
for x being set ex y being set st S₁[n,x,y]

proof

let n be 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
A2: dom f = NAT and
A3: f . 0 = G and
A4: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
reconsider f = f as NAT -defined Function by A2, RELAT_1:def 18;
reconsider f = f as ManySortedSet of NAT by A2, 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 A3; :: 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 A5: G = myc . k ; :: thesis: myc . (k + 1) = Mycielskian G
ex G being SimpleGraph st
( f . k = G & f . (k + 1) = Mycielskian G ) by A4, A5;
hence myc . (k + 1) = Mycielskian G by A5; :: thesis: verum