Aa: card 2 = 2 by CARD_1:50, CARD_2:57;
set P2 = CompleteSGraph 2;
defpred S₁[ Nat] means ( clique# ((MycielskianSeq (CompleteSGraph 2)) . $1) = 2 & chromatic# ((MycielskianSeq (CompleteSGraph 2)) . $1) = $1 + 2 );
A: clique# ((MycielskianSeq (CompleteSGraph 2)) . 0) = clique# (CompleteSGraph 2) by MSeq0
.= 2 by Aa, cliqueCSG ;
chromatic# ((MycielskianSeq (CompleteSGraph 2)) . 0) = chromatic# (CompleteSGraph 2) by MSeq0
.= 0 + 2 by Aa, chromaticCSG ;
then P0: S₁[ 0 ] by A;
P1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume IH: S₁[n] ; :: thesis: S₁[n + 1]
thus clique# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = clique# (Mycielskian ((MycielskianSeq (CompleteSGraph 2)) . n)) by MSeq1
.= 2 by MClique, IH ; :: thesis: chromatic# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = (n + 1) + 2
thus chromatic# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = chromatic# (Mycielskian ((MycielskianSeq (CompleteSGraph 2)) . n)) by MSeq1
.= 1 + (n + 2) by IH, Mcn1
.= (n + 1) + 2 ; :: thesis: verum

end;

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