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 b1 is ext-natural )
assume x in {N,M,K} ; :: thesis: b1 is ext-natural
per cases then ( x = N or x = M or x = K ) by ENUMSET1:def 1;
end;
end;
hence {N,M,K} is ext-natural-membered ; :: thesis: verum