theorem Th5: :: STIRL2_1:5

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