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

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

per cases then ( x = N or x = M ) by TARSKI:def 2;

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;

end;

end;

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