let n be Nat; :: thesis: union (OpenHypercubesRAT n) is countable
for Y being set st Y in OpenHypercubesRAT n holds
Y is countable
proof
let Y be set ; :: thesis: ( Y in OpenHypercubesRAT n implies Y is countable )
assume A2: Y in OpenHypercubesRAT n ; :: thesis: Y is countable
consider q0 being Point of (Euclid n) such that
A3: Y = OpenHypercubes q0 and
q0 in RAT n by A2;
thus Y is countable by A3; :: thesis: verum
end;
hence union (OpenHypercubesRAT n) is countable by CARD_4:12; :: thesis: verum