set F1 = { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ;
set F2 = { F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } ;
A1: { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } is finite from FINSEQ_1:sch 6();
{ F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } c= { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } or x in { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } )
assume x in { F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } ; :: thesis: x in { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) }
then ex i being Element of NAT st
( F₃(i) = x & F₁() < i & i <= F₂() & P₁[i] ) ;
hence x in { F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[i] ) } ; :: thesis: verum

end;

hence { F₃(i) where i is Element of NAT : ( F₁() < i & i <= F₂() & P₁[i] ) } is finite by A1; :: thesis: verum