theorem Th27: :: GRAPHSP:27

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