let A be Subset of R^1; :: thesis: ( A is closed & A is open & not A = {} implies A = REAL )
assume ( A is closed & A is open ) ; :: thesis: ( A = {} or A = REAL )
then reconsider A = A as open closed Subset of R^1 ;
( A = {} or A = [#] R^1 ) by Th32;
hence ( A = {} or A = REAL ) by TOPMETR:17; :: thesis: verum