theorem :: FINTOPO3:21

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