theorem :: FINTOPO3:38

for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fdfl (A,(n + 1)) = (Fdfl (A,n)) ^d by Def8;