let A be Subset of Niemytzki-plane; :: thesis: ( A = y>=0-plane \ y=0-line implies Cl A = [#] Niemytzki-plane )
A \ {A} = A
proof
thus A \ {A} c= A by XBOOLE_1:36; :: according to XBOOLE_0:def 10 :: thesis: A c= A \ {A}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A \ {A} )
not A in A ;
hence ( not x in A or x in A \ {A} ) by ZFMISC_1:56; :: thesis: verum
end;
hence ( A = y>=0-plane \ y=0-line implies Cl A = [#] Niemytzki-plane ) by Th33; :: thesis: verum