let n be Element of NAT ; :: thesis: min* n = 0

now

per cases ( 0 = n or 0 < n ) ;

suppose 0 = n ; :: thesis: min* n = 0

hence min* n = 0 by NAT_1:def 1; :: thesis: verum

end;

suppose 0 < n ; :: thesis: min* n = 0

then 0 in { l where l is Element of NAT : l < n } ;
then ( 0 in n & n is Subset of NAT ) by Th8, AXIOMS:30;
hence min* n = 0 by NAT_1:def 1; :: thesis: verum

end;

end;

end;

hence min* n = 0 ; :: thesis: verum