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