let n be Element of NAT ; :: thesis: ( min* {n} = n & min {n} = n )
A1: min* {n} in {n} by NAT_1:def 1;
min* {n} = min {n} by Th1;
hence ( min* {n} = n & min {n} = n ) by A1, TARSKI:def 1; :: thesis: verum