set T = { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ;
set S = { F₃(n) where n is Element of NAT : n <= F₁() } ;

A1: 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 : ( 0 <= n & n <= F₁() ) } ) & ( x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } 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 : ( 0 <= n & n <= F₁() ) } ) & ( x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } 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 : ( 0 <= n & n <= F₁() ) } 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 : ( 0 <= n & n <= F₁() ) }
then ex n being Element of NAT st
( x = F₃(n) & n <= F₁() ) ;
hence x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ; :: thesis: verum

end;

assume x in { F₃(n) where n is Element of NAT : ( 0 <= n & n <= F₁() ) } ; :: thesis: x in { F₃(n) where n is Element of NAT : n <= F₁() }
then ex n being Element of NAT st
( x = F₃(n) & 0 <= n & n <= F₁() ) ;
hence x in { F₃(n) where n is Element of NAT : n <= F₁() } ; :: thesis: verum

end;

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