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

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