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