let n be Element of NAT ; :: thesis: for f being Element of REAL * holds OuterVx (f,n) c= Seg n
let f be Element of REAL * ; :: thesis: OuterVx (f,n) c= Seg n
( OuterVx (f,n) c= UnusedVx (f,n) & UnusedVx (f,n) c= Seg n ) by Th27, Th28;
hence OuterVx (f,n) c= Seg n by XBOOLE_1:1; :: thesis: verum