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
Fcl A,n c= Fcl A,m
let A be Subset of FT; :: thesis: for n, m being Element of NAT st n <= m holds
Fcl A,n c= Fcl A,m
let n, m be Element of NAT ; :: thesis: ( n <= m implies Fcl A,n c= Fcl A,m )
defpred S₁[ Element of NAT ] means Fcl A,n c= Fcl A,(n + $1);
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A2: Fcl A,(n + k) c= Fcl A,((n + k) + 1) by FINTOPO3:25;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A2, XBOOLE_1:1; :: thesis: verum

end;

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