reconsider A = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) as dense Subset of Niemytzki-plane by Th36;
A1: card A c= card (product <*RAT,RAT*>) by CARD_1:11, XBOOLE_1:17;
density Niemytzki-plane c= card A by TOPGEN_1:def 12;
then density Niemytzki-plane c= card (product <*RAT,RAT*>) by A1;
hence density Niemytzki-plane c= omega by Th8, CARD_4:6, TOPGEN_3:17; :: according to TOPGEN_1:def 13 :: thesis: verum