let n be Nat; :: thesis: for N being non empty Subset of NAT st N c= n & N <> {(n - 1)} holds
min* N < n - 1
let N be non empty Subset of NAT; :: thesis: ( N c= n & N <> {(n - 1)} implies min* N < n - 1 )
assume that
A1: N c= n and
A2: N <> {(n - 1)} and
A3: min* N >= n - 1 ; :: thesis: contradiction

now

let k be set ; :: thesis: ( k in N implies k in {(n - 1)} )
assume A4: k in N ; :: thesis: k in {(n - 1)}
reconsider k9 = k as Element of NAT by A4;
min* N <= k9 by A4, NAT_1:def 1;
then A5: n - 1 <= k9 by A3, XXREAL_0:2;
k9 <= n - 1 by A1, A4, Th10;
then n - 1 = k by A5, XXREAL_0:1;
hence k in {(n - 1)} by TARSKI:def 1; :: thesis: verum

end;

then N c= {(n - 1)} by TARSKI:def 3;
hence contradiction by A2, ZFMISC_1:39; :: thesis: verum