let n be Nat; :: thesis: min* n = 0

now :: thesis: min* n = 0

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 Nat : l < n } ;
then A1: 0 in n by AXIOMS:4;
n is Subset of NAT by Th8;
hence min* n = 0 by A1, NAT_1:def 1; :: thesis: verum

end;

end;

end;

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