now :: thesis: for i being Nat st i in (Seg n) /\ (dom R) holds
R . i >= 0

let i be Nat; :: thesis: ( i in (Seg n) /\ (dom R) implies R . i >= 0 )
assume i in (Seg n) /\ (dom R) ; :: thesis: R . i >= 0
then i in dom R by XBOOLE_0:def 4;
then R . i in rng R by FUNCT_1:def 3;
hence R . i >= 0 by PARTFUN3:def 4; :: thesis: verum

end;

hence not ClosedHypercube (p,R) is empty by Th5; :: thesis: verum