let FT be non empty filled RelStr ; :: thesis: for A being Subset of
for n, m being Element of NAT st n <= m holds
Fdfl A,m c= Fdfl A,n
let A be Subset of ; :: 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 S₁[ Element of NAT ] means Fdfl A,(n + $1) c= Fdfl A,n;
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: Fdfl A,((n + k) + 1) c= Fdfl A,(n + k) by FINTOPO3:44;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[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: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 Fdfl A,m c= Fdfl A,n by A3; :: thesis: verum