let FT be non empty filled RelStr ; :: thesis: for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
let A be Subset of FT; :: thesis: for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
let n, m be Element of NAT ; :: thesis: ( n <= m implies Finf (A,n) c= Finf (A,m) )
defpred S₁[ Nat] means Finf (A,n) c= Finf (A,(n + $1));
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A2: Finf (A,(n + k)) c= Finf (A,((n + k) + 1)) by FINTOPO3:37;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A2, XBOOLE_1:1; :: thesis: verum

end;

assume n <= m ; :: thesis: Finf (A,n) c= Finf (A,m)
then m - n >= 0 by XREAL_1:48;
then A3: n + (m -' n) = n + (m - n) by XREAL_0:def 2
.= m ;
A4: S₁[ 0 ] ;
for m2 being Nat holds S₁[m2] from NAT_1:sch 2(A4, A1);
hence Finf (A,n) c= Finf (A,m) by A3; :: thesis: verum