let A be Subset of Niemytzki-plane; :: thesis: ( A = y=0-line implies ( Cl A = A & Int A = {} ) )
assume A1: A = y=0-line ; :: thesis: ( Cl A = A & Int A = {} )
then A2: A ` = y>=0-plane \ y=0-line by Def3;
thus Cl A = A by A1, Th26, PRE_TOPC:22; :: thesis: Int A = {}
thus Int A = (Cl (A `)) ` by TOPS_1:def 1
.= ([#] Niemytzki-plane) ` by A2, Th34
.= {} by XBOOLE_1:37 ; :: thesis: verum