let n, k be Element of NAT ; :: thesis: ( min* {n,k} = min (n,k) & min {n,k} = min (n,k) )
A1: min {n} = n by Th5;
{n,k} = {n} \/ {k} by ENUMSET1:1;
then A2: min {n,k} = min ((min {n}),(min {k})) by Th2;
min {n,k} = min* {n,k} by Th1;
hence ( min* {n,k} = min (n,k) & min {n,k} = min (n,k) ) by A2, A1, Th5; :: thesis: verum