let n be Element of 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 k' = k as Element of NAT by A4;
( min* N <= k' & k' in n ) by A1, A4, NAT_1:def 1;
then ( n - 1 <= k' & k' <= n - 1 ) by A3, Th10, XXREAL_0:2;
then n - 1 = k by 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