let n be Nat; :: thesis: for N being non empty Subset of NAT st N c= Segm n & N <> {(n - 1)} holds

min* N < n - 1

let N be non empty Subset of NAT; :: thesis: ( N c= Segm n & N <> {(n - 1)} implies min* N < n - 1 )

assume that

A1: N c= Segm n and

A2: N <> {(n - 1)} and

A3: min* N >= n - 1 ; :: thesis: contradiction

hence contradiction by A2, ZFMISC_1:33; :: thesis: verum

min* N < n - 1

let N be non empty Subset of NAT; :: thesis: ( N c= Segm n & N <> {(n - 1)} implies min* N < n - 1 )

assume that

A1: N c= Segm n and

A2: N <> {(n - 1)} and

A3: min* N >= n - 1 ; :: thesis: contradiction

now :: thesis: for k being object st k in N holds

k in {(n - 1)}

then
N c= {(n - 1)}
;k in {(n - 1)}

let k be object ; :: 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;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

hence contradiction by A2, ZFMISC_1:33; :: thesis: verum