defpred S2[ Nat, object , object ] means ( ( $2 is NatRelStr of (3 * (2 |^ $1)) -' 1 implies ex R being NatRelStr of (3 * (2 |^ $1)) -' 1 st
( $2 = R & $3 = Mycielskian R ) ) & ( $2 is not NatRelStr of (3 * (2 |^ $1)) -' 1 implies $3 = $2 ) );
A1: for n being Nat
for x being set ex y being set st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S2[n,x,y]
let x be set ; :: thesis: ex y being set st S2[n,x,y]
per cases ( x is NatRelStr of (3 * (2 |^ n)) -' 1 or not x is NatRelStr of (3 * (2 |^ n)) -' 1 ) ;
suppose x is NatRelStr of (3 * (2 |^ n)) -' 1 ; :: thesis: ex y being set st S2[n,x,y]
then reconsider R = x as NatRelStr of (3 * (2 |^ n)) -' 1 ;
Mycielskian R = Mycielskian R ;
then consider y being object such that
A2: S2[n,x,y] ;
 y is set by TARSKI:1;
hence ex y being set st S2[n,x,y] by A2; :: thesis: verum
end;
suppose x is not NatRelStr of (3 * (2 |^ n)) -' 1 ; :: thesis: ex y being set st S2[n,x,y]
hence ex y being set st S2[n,x,y] ; :: thesis: verum
end;
end;
end;
consider f being Function such that
A3: dom f = NAT and
A4: f . 0 = CompleteRelStr 2 and
A5: for n being Nat holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
 defpred S3[ Nat] means f . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1;
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then A6: S3[ 0 ] by A4;
A7: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A8: S3[k] ; :: thesis: S3[k + 1]
consider R being NatRelStr of (3 * (2 |^ k)) -' 1 such that
f . k = R and
A9: f . (k + 1) = Mycielskian R by A8, A5;
A10: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;
then 2 |^ k >= 1 by XXREAL_0:2;
then A11: 3 * (2 |^ k) >= 1 by A10, XXREAL_0:2;
then A12: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;
then 3 * (2 |^ (k + 1)) >= 1 by A11, XXREAL_0:2;
then A13: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A12, XREAL_0:def 2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6
.= (3 * (2 |^ (k + 1))) -' 1 by A13, XREAL_0:def 2 ;
hence S3[k + 1] by A9; :: thesis: verum
end;
A14: for n being Nat holds S3[n] from NAT_1:sch 2(A6, A7);
 reconsider IT = f . n as NatRelStr of (3 * (2 |^ n)) -' 1 by A14;
take IT ; :: thesis: ex myc being Function st
( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
take myc = f; :: thesis: ( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus IT = myc . n ; :: thesis: ( dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus dom myc = NAT by A3; :: thesis: ( myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus myc . 0 = CompleteRelStr 2 by A4; :: thesis: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
let k be Nat; :: thesis: for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
let R be NatRelStr of (3 * (2 |^ k)) -' 1; :: thesis: ( R = myc . k implies myc . (k + 1) = Mycielskian R )
assume A15: R = myc . k ; :: thesis: myc . (k + 1) = Mycielskian R
then consider RR being NatRelStr of (3 * (2 |^ k)) -' 1 such that
A16: f . k = RR and
A17: f . (k + 1) = Mycielskian RR by A5;
thus myc . (k + 1) = Mycielskian R by A17, A15, A16; :: thesis: verum