theorem Th26: :: GRAPHSP:26

for n being Nat
for f being Element of REAL * holds UnusedVx (f,n) c= Seg n