theorem Th28: :: GRAPHSP:28

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