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