reconsider A = (y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) as dense Subset of Niemytzki-plane by Th40;
A1: card A c= card (product <*RAT ,RAT *>) by CARD_1:27, 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, XBOOLE_1:1;
hence density Niemytzki-plane c= omega by Th12, CARD_4:54, TOPGEN_3:17; :: according to TOPGEN_1:def 13 :: thesis: verum