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:41;
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