reconsider B = y=0-line as Subset of Niemytzki-plane by Def3, Th19;
reconsider A = y>=0-plane \ y=0-line as open Subset of Niemytzki-plane by Th25;
B ` = A by Def3;
then A ` = y=0-line ;
hence y=0-line is closed Subset of Niemytzki-plane ; :: thesis: verum