let n be Nat; :: thesis: union (OpenHypercubesRAT n) is Subset-Family of (TOP-REAL n)
union (OpenHypercubesRAT n) c= bool the carrier of (TOP-REAL n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (OpenHypercubesRAT n) or x in bool the carrier of (TOP-REAL n) )
assume x in union (OpenHypercubesRAT n) ; :: thesis: x in bool the carrier of (TOP-REAL n)
then consider y being set such that
A1: x in y and
A2: y in OpenHypercubesRAT n by TARSKI:def 4;
consider q0 being Point of (Euclid n) such that
A3: y = OpenHypercubes q0 and
q0 in RAT n by A2;
x in bool (REAL n) by A1, A3;
hence x in bool the carrier of (TOP-REAL n) by EUCLID:22; :: thesis: verum
end;
hence union (OpenHypercubesRAT n) is Subset-Family of (TOP-REAL n) ; :: thesis: verum