let X be Element of union (rng sequence_univers); :: thesis: for n being Nat st rank_univers X <= n holds
X in sequence_univers . n
let n be Nat; :: thesis: ( rank_univers X <= n implies X in sequence_univers . n )
assume A1: rank_univers X <= n ; :: thesis: X in sequence_univers . n
defpred S₁[ Nat] means X in sequence_univers . $1;
A2: S₁[ rank_univers X] by Def13;
A3: for j being Nat st rank_univers X <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( rank_univers X <= j & S₁[j] implies S₁[j + 1] )
assume that
rank_univers X <= j and
A4: S₁[j] ; :: thesis: S₁[j + 1]
sequence_univers . j c= sequence_univers . (j + 1) by Th105;
hence S₁[j + 1] by A4; :: thesis: verum

end;

for i being Nat st rank_univers X <= i holds
S₁[i] from NAT_1:sch 8(A2, A3);
hence X in sequence_univers . n by A1; :: thesis: verum