theorem :: FINTOPO3:32

for T being non empty RelStr
for A being Subset of T holds Finf (A,0) = A by Def6;