let n be Element of NAT ; :: thesis: for D being non empty Subset of (TOP-REAL 2) holds width (Gauge D,n) = (2 |^ n) + 3
let D be non empty Subset of (TOP-REAL 2); :: thesis: width (Gauge D,n) = (2 |^ n) + 3
thus width (Gauge D,n) = len (Gauge D,n) by JORDAN8:def 1
.= (2 |^ n) + 3 by JORDAN8:def 1 ; :: thesis: verum