let n be Nat; :: thesis: union (OpenHypercubesRAT n) is open Subset-Family of (TOP-REAL n)
reconsider UO = union (OpenHypercubesRAT n) as Subset-Family of (TOP-REAL n) by Th18;
UO is open

proof

let P be Subset of (TOP-REAL n); :: according to TOPS_2:def 1 :: thesis: ( not P in UO or P is simplex-like )
assume P in UO ; :: thesis: P is simplex-like
then consider X being set such that
A1: P in X and
A2: X in OpenHypercubesRAT n by TARSKI:def 4;
consider q0 being Point of (Euclid n) such that
A3: X = OpenHypercubes q0 and
q0 in RAT n by A2;
A4: OpenHypercubes q0 is open ;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P0 = P as Subset of (TopSpaceMetr (Euclid n)) ;
P0 is open by A4, A3, A1;
hence P is simplex-like by Th10; :: thesis: verum

end;

hence union (OpenHypercubesRAT n) is open Subset-Family of (TOP-REAL n) ; :: thesis: verum