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
Fdfl (A,m) c= Fdfl (A,n)
let A be Subset of FT; :: thesis: for n, m being Element of NAT st n <= m holds
Fdfl (A,m) c= Fdfl (A,n)
let n, m be Element of NAT ; :: thesis: ( n <= m implies Fdfl (A,m) c= Fdfl (A,n) )
defpred S1[ Nat] means Fdfl (A,(n + $1)) c= Fdfl (A,n);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A2: Fdfl (A,((n + k) + 1)) c= Fdfl (A,(n + k)) by FINTOPO3:44;
assume S1[k] ; :: thesis: S1[k + 1]
hence S1[k + 1] by A2, XBOOLE_1:1; :: thesis: verum
end;
assume n <= m ; :: thesis: Fdfl (A,m) c= Fdfl (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: S1[ 0 ] ;
for m2 being Nat holds S1[m2] from NAT_1:sch 2(A4, A1);
 hence Fdfl (A,m) c= Fdfl (A,n) by A3; :: thesis: verum