theorem :: FINTOPO3:41

for T being non empty RelStr
for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d