theorem :: FINTOPO3:35

for T being non empty RelStr
for A, B being Subset of T
for n being Nat holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))