defpred S₁[ Element of 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 Element of NAT such that
A2: i is_sufficiently_large_for C by Lm2;
i in { i where i is Element of NAT : S₁[i] } by A2;
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 Element of 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 Element of NAT st j is_sufficiently_large_for C holds
j >= min X
let j be Element of NAT ; :: thesis: ( j is_sufficiently_large_for C implies j >= min X )
assume j is_sufficiently_large_for C ; :: thesis: j >= min X
then j in X ;
hence j >= min X by XXREAL_2:def 7; :: thesis: verum