defpred S₁[ Nat] means $1 is_sufficiently_large_for C;
set X = { i where i is Element of NAT : S₁[i] } ;
A1: { i where i is Element of NAT : S₁[i] } is Subset of NAT from DOMAIN_1:sch 7();
consider i being Nat such that
A2: i is_sufficiently_large_for C by Lm2;
A3: i in NAT by ORDINAL1:def 12;
i in { i where i is Element of NAT : S₁[i] } by A2, A3;
then reconsider X = { i where i is Element of NAT : S₁[i] } as non empty Subset of NAT by A1;
take min X ; :: thesis: ( min X is_sufficiently_large_for C & ( for j being Nat st j is_sufficiently_large_for C holds
j >= min X ) )
min X in X by XXREAL_2:def 7;
then ex i being Element of NAT st
( i = min X & i is_sufficiently_large_for C ) ;
hence min X is_sufficiently_large_for C ; :: thesis: for j being Nat st j is_sufficiently_large_for C holds
j >= min X
let j be Nat; :: thesis: ( j is_sufficiently_large_for C implies j >= min X )
A4: j in NAT by ORDINAL1:def 12;
assume j is_sufficiently_large_for C ; :: thesis: j >= min X
then j in X by A4;
hence j >= min X by XXREAL_2:def 7; :: thesis: verum