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
A1: OuterVx f,n c= UnusedVx f,n by Th28;
UnusedVx f,n c= Seg n by Th27;
hence OuterVx f,n c= Seg n by A1, XBOOLE_1:1; :: thesis: verum