A1: card 2 = 2 ;
set P2 = CompleteSGraph 2;
defpred S₁[ Nat] means ( clique# ((MycielskianSeq (CompleteSGraph 2)) . $1) = 2 & chromatic# ((MycielskianSeq (CompleteSGraph 2)) . $1) = $1 + 2 );
A2: clique# ((MycielskianSeq (CompleteSGraph 2)) . 0) = clique# (CompleteSGraph 2) by Th113
.= 2 by A1, Th59 ;
chromatic# ((MycielskianSeq (CompleteSGraph 2)) . 0) = chromatic# (CompleteSGraph 2) by Th113
.= 0 + 2 by A1, Th69 ;
then A3: S₁[ 0 ] by A2;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
thus clique# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = clique# (Mycielskian ((MycielskianSeq (CompleteSGraph 2)) . n)) by Th115
.= 2 by Th110, A5 ; :: thesis: chromatic# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = (n + 1) + 2
thus chromatic# ((MycielskianSeq (CompleteSGraph 2)) . (n + 1)) = chromatic# (Mycielskian ((MycielskianSeq (CompleteSGraph 2)) . n)) by Th115
.= 1 + (n + 2) by A5, Th112
.= (n + 1) + 2 ; :: thesis: verum

end;

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