set S = { F₃(n) where n is Element of NAT : n < F₁() } ;
consider m being Nat such that
A2: F₁() = m + 1 by A1, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
set T = { F₃(n) where n is Element of NAT : n <= m } ;

A3: now :: thesis: for x being object holds
( ( x in { F₃(n) where n is Element of NAT : n < F₁() } implies x in { F₃(n) where n is Element of NAT : n <= m } ) & ( x in { F₃(n) where n is Element of NAT : n <= m } implies x in { F₃(n) where n is Element of NAT : n < F₁() } ) )

let x be object ; :: thesis: ( ( x in { F₃(n) where n is Element of NAT : n < F₁() } implies x in { F₃(n) where n is Element of NAT : n <= m } ) & ( x in { F₃(n) where n is Element of NAT : n <= m } implies x in { F₃(n) where n is Element of NAT : n < F₁() } ) )

hereby :: thesis: ( x in { F₃(n) where n is Element of NAT : n <= m } implies x in { F₃(n) where n is Element of NAT : n < F₁() } )

assume x in { F₃(n) where n is Element of NAT : n < F₁() } ; :: thesis: x in { F₃(n) where n is Element of NAT : n <= m }
then consider n being Element of NAT such that
A4: x = F₃(n) and
A5: n < F₁() ;
n <= m by A2, A5, NAT_1:13;
hence x in { F₃(n) where n is Element of NAT : n <= m } by A4; :: thesis: verum

end;

assume x in { F₃(n) where n is Element of NAT : n <= m } ; :: thesis: x in { F₃(n) where n is Element of NAT : n < F₁() }
then consider n being Element of NAT such that
A6: x = F₃(n) and
A7: n <= m ;
n < m + 1 by A7, NAT_1:13;
hence x in { F₃(n) where n is Element of NAT : n < F₁() } by A2, A6; :: thesis: verum

end;

{ F₃(n) where n is Element of NAT : n <= m } is non empty finite Subset of F₂() from ASYMPT_0:sch 2();
hence { F₃(n) where n is Element of NAT : n < F₁() } is non empty finite Subset of F₂() by A3, TARSKI:2; :: thesis: verum