let n be 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