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

let r be Element of REAL ; :: thesis:
assume r in dom tan ; :: thesis:
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:

end;