set S = { F3(n) where n is Element of NAT : n < F1() } ;
consider m being Nat such that
A2: F1() = m + 1 by A1, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
set T = { F3(n) where n is Element of NAT : n <= m } ;
A3: now :: thesis: for x being object holds
( ( x in { F3(n) where n is Element of NAT : n < F1() } implies x in { F3(n) where n is Element of NAT : n <= m } ) & ( x in { F3(n) where n is Element of NAT : n <= m } implies x in { F3(n) where n is Element of NAT : n < F1() } ) )
let x be object ; :: thesis: ( ( x in { F3(n) where n is Element of NAT : n < F1() } implies x in { F3(n) where n is Element of NAT : n <= m } ) & ( x in { F3(n) where n is Element of NAT : n <= m } implies x in { F3(n) where n is Element of NAT : n < F1() } ) )
hereby :: thesis: ( x in { F3(n) where n is Element of NAT : n <= m } implies x in { F3(n) where n is Element of NAT : n < F1() } )
assume x in { F3(n) where n is Element of NAT : n < F1() } ; :: thesis: x in { F3(n) where n is Element of NAT : n <= m }
then consider n being Element of NAT such that
A4: x = F3(n) and
A5: n < F1() ;
n <= m by A2, A5, NAT_1:13;
hence x in { F3(n) where n is Element of NAT : n <= m } by A4; :: thesis: verum
end;
assume x in { F3(n) where n is Element of NAT : n <= m } ; :: thesis: x in { F3(n) where n is Element of NAT : n < F1() }
then consider n being Element of NAT such that
A6: x = F3(n) and
A7: n <= m ;
n < m + 1 by A7, NAT_1:13;
hence x in { F3(n) where n is Element of NAT : n < F1() } by A2, A6; :: thesis: verum
end;
{ F3(n) where n is Element of NAT : n <= m } is non empty finite Subset of F2() from ASYMPT_0:sch 2();
 hence { F3(n) where n is Element of NAT : n < F1() } is non empty finite Subset of F2() by A3, TARSKI:2; :: thesis: verum