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