theorem :: FINTOPO3:19

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