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