defpred S₁[ Nat] means ( clique# (Mycielskian $1) = 2 & chromatic# (Mycielskian $1) = $1 + 2 );
P0: clique# (Mycielskian 0) = clique# (CompleteRelStr 2) by Mycn1
.= 2 by CompleteCli ;
chromatic# (Mycielskian 0) = chromatic# (CompleteRelStr 2) by Mycn1
.= 2 by CompleteChr ;
then P1: S₁[ 0 ] by P0;
P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A: clique# (Mycielskian n) = 2 and
B: chromatic# (Mycielskian n) = n + 2 ; :: thesis: S₁[n + 1]
C: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Mycn1;
thus clique# (Mycielskian (n + 1)) = 2 by A, C, MClique; :: thesis: chromatic# (Mycielskian (n + 1)) = (n + 1) + 2
thus chromatic# (Mycielskian (n + 1)) = 1 + (chromatic# (Mycielskian n)) by C, Mchromatic
.= (n + 1) + 2 by B ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence for n being Nat holds
( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 ) ; :: thesis: verum