begin
Lm1:
for r being Real st r > 0 holds
ex n being Element of NAT st
( 1 / n < r & n > 0 )
Lm2:
for T being TopStruct
for A being Subset of T holds
( A is open iff ([#] T) \ A is closed )
theorem Th13:
for
A,
B being
set st
B c= A holds
(id A) .: B = B
begin
begin
Lm3:
{REAL} c= the carrier of REAL?
begin
:: Preliminaries
::