consider myc being Function such that
A1: Mycielskian 0 = myc . 0 and
dom myc = NAT and
A2: myc . 0 = CompleteRelStr 2 and
for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R by Def10;
thus Mycielskian 0 = CompleteRelStr 2 by A1, A2; :: thesis: for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k)
let k be Nat; :: thesis: Mycielskian (k + 1) = Mycielskian (Mycielskian k)
consider myc1 being Function such that
A3: Mycielskian k = myc1 . k and
A4: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R ) ) by Def10;
consider myc2 being Function such that
A5: Mycielskian (k + 1) = myc2 . (k + 1) and
A6: ( dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 ) and
A7: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R by Def10;
myc1 = myc2 by A4, A6, A7, Lm1;
hence Mycielskian (k + 1) = Mycielskian (Mycielskian k) by A3, A7, A5; :: thesis: verum