set T = dom tan;
for r being Element of REAL st r in dom tan holds
ex N being Neighbourhood of r st N c= dom tan

proof

let r be Element of REAL ; :: thesis: ( r in dom tan implies ex N being Neighbourhood of r st N c= dom tan )
assume r in dom tan ; :: thesis: ex N being Neighbourhood of r st N c= dom tan
then consider X being set such that
A1: ( r in X & X in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } ) by Th16, TARSKI:def 4;
consider i being Integer such that
A2: X = ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ by A1;
consider N being Neighbourhood of r such that
A3: N c= X by A1, A2, RCOMP_1:18;
X c= dom tan by A1, Th16, ZFMISC_1:74;
hence ex N being Neighbourhood of r st N c= dom tan by A3, XBOOLE_1:1; :: thesis: verum

end;

hence for b₁ being Subset of REAL st b₁ = dom tan holds
b₁ is open by RCOMP_1:20; :: thesis: verum