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
Fint (A,m) c= Fint (A,n)
let A be Subset of FT; :: thesis: for n, m being Element of NAT st n <= m holds
Fint (A,m) c= Fint (A,n)
let n, m be Element of NAT ; :: thesis: ( n <= m implies Fint (A,m) c= Fint (A,n) )
defpred S₁[ Nat] means Fint (A,(n + $1)) c= Fint (A,n);
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: Fint (A,((n + k) + 1)) c= Fint (A,(n + k)) by FINTOPO3:26;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A2, XBOOLE_1:1; :: thesis: verum

end;

assume n <= m ; :: thesis: Fint (A,m) c= Fint (A,n)
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 Fint (A,m) c= Fint (A,n) by A3; :: thesis: verum