let n be Nat; :: thesis: not union (OpenHypercubesRAT n) is empty
assume union (OpenHypercubesRAT n) is empty ; :: thesis: contradiction
then A1: OpenHypercubesRAT n = {{}} by SCMYCIEL:18;
not OpenHypercubesRAT n is empty ;
then consider x being object such that
A2: x in OpenHypercubesRAT n ;
consider q being Point of (Euclid n) such that
A3: x = OpenHypercubes q and
q in RAT n by A2;
thus contradiction by A3, A1, A2, TARSKI:def 1; :: thesis: verum