let n be Nat; :: thesis: ( n >= 1 implies for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded )
assume A1: n >= 1 ; :: thesis: for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded
REAL n c= the carrier of (Euclid n) ;
then reconsider W = REAL n as Subset of (Euclid n) ;
let P be Subset of (Euclid n); :: thesis: ( P is bounded implies not P ` is bounded )
A2: P \/ (P `) = [#] (Euclid n) by PRE_TOPC:2
.= W ;
assume ( P is bounded & P ` is bounded ) ; :: thesis: contradiction
hence contradiction by A1, A2, JORDAN2C:33, TBSP_1:13; :: thesis: verum