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