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

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