let n be Element of 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
let P be Subset of (Euclid n); :: thesis: ( P is bounded implies not P ` is bounded )
REAL n c= the carrier of (Euclid n) ;
then reconsider W = REAL n as Subset of (Euclid n) ;
assume A2: ( P is bounded & P ` is bounded ) ; :: thesis: contradiction
P \/ (P ` ) = [#] (Euclid n) by PRE_TOPC:18
.= W ;
hence contradiction by A1, A2, JORDAN2C:39, TBSP_1:20; :: thesis: verum