theorem Th6: :: STIRL2_1:6

for n, k being Element of NAT holds
( min* {n,k} = min (n,k) & min {n,k} = min (n,k) )