theorem Th7: :: FINTOPO5:7

for T being non empty RelStr
for p being Element of T
for k being Nat st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))