let A be set ; :: thesis: ( A c= [:REAL,REAL,REAL:] & A /\ [:RAT,RAT,RAT:] <> {} implies ex p being sequence of [:REAL,REAL,REAL:] st rng p = A /\ [:RAT,RAT,RAT:] )
assume that
A1: A c= [:REAL,REAL,REAL:] and
A2: A /\ [:RAT,RAT,RAT:] <> {} ; :: thesis: ex p being sequence of [:REAL,REAL,REAL:] st rng p = A /\ [:RAT,RAT,RAT:]
[:RAT,RAT:] is countable by CARD_4:7;
then [:RAT,RAT,RAT:] is countable by CARD_4:7;
then A /\ [:RAT,RAT,RAT:] is countable by CARD_3:94;
then consider f being Function of omega,(A /\ [:RAT,RAT,RAT:]) such that
A3: rng f = A /\ [:RAT,RAT,RAT:] by CARD_3:96, A2;
A /\ [:RAT,RAT,RAT:] c= A by XBOOLE_1:17;
then rng f c= [:REAL,REAL,REAL:] by A1;
then reconsider f = f as sequence of [:REAL,REAL,REAL:] by A2, FUNCT_2:6;
take f ; :: thesis: rng f = A /\ [:RAT,RAT,RAT:]
thus rng f = A /\ [:RAT,RAT,RAT:] by A3; :: thesis: verum