consider Y being set such that
A1: X in Y and
A2: Y in rng (sequence_univers {}) by TARSKI:def 4;
consider x being object such that
A3: x in dom (sequence_univers {}) and
A4: Y = (sequence_univers {}) . x by A2, FUNCT_1:def 3;
x in NAT by A3, Def9;
then reconsider x = x as Nat ;
defpred S₁[ Nat] means X in sequence_univers . $1;
X in (sequence_univers {}) . x by A1, A4;
then A5: ex k being Nat st S₁[k] ;
consider k being Nat such that
A6: S₁[k] and
A7: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A5);
take k ; :: thesis: ( X in sequence_univers . k & ( for n being Nat st n < k holds
not X in sequence_univers . n ) )
thus ( X in sequence_univers . k & ( for n being Nat st n < k holds
not X in sequence_univers . n ) ) by A6, A7; :: thesis: verum