set T = { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ;
set S = { F3(n) where n is Element of NAT : n <= F1() } ;
A1: 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 : ( 0 <= n & n <= F1() ) } ) & ( x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } 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 : ( 0 <= n & n <= F1() ) } ) & ( x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } 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 : ( 0 <= n & n <= F1() ) } 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 : ( 0 <= n & n <= F1() ) }
then ex n being Element of NAT st
( x = F3(n) & n <= F1() ) ;
hence x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ; :: thesis: verum
end;
assume x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ; :: thesis: x in { F3(n) where n is Element of NAT : n <= F1() }
then ex n being Element of NAT st
( x = F3(n) & 0 <= n & n <= F1() ) ;
hence x in { F3(n) where n is Element of NAT : n <= F1() } ; :: thesis: verum
end;
A2: 0 <= F1() ;
{ F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } is non empty finite Subset of F2() from ASYMPT_0:sch 1(A2);
 hence { F3(n) where n is Element of NAT : n <= F1() } is non empty finite Subset of F2() by A1, TARSKI:2; :: thesis: verum