theorem :: FINTOPO3:34

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