let X be Subset of R^1; :: according to TSEP_1:def 1 :: thesis: ( not X = the carrier of (R^1 | (R^1 A)) or X is open )
assume X = the carrier of (R^1 | (R^1 A)) ; :: thesis: X is open
hence X is open by PRE_TOPC:8; :: thesis: verum