now :: thesis: for x being object st x in {N,M,K} holds
x is ext-natural

let x be object ; :: thesis: ( x in {N,M,K} implies b₁ is ext-natural )
assume x in {N,M,K} ; :: thesis: b₁ is ext-natural

per cases then ( x = N or x = M or x = K ) by ENUMSET1:def 1;

suppose x = N ; :: thesis: b₁ is ext-natural

hence x is ext-natural ; :: thesis: verum

end;

suppose x = M ; :: thesis: b₁ is ext-natural

hence x is ext-natural ; :: thesis: verum

end;

suppose x = K ; :: thesis: b₁ is ext-natural

hence x is ext-natural ; :: thesis: verum

end;

end;

end;

hence {N,M,K} is ext-natural-membered ; :: thesis: verum