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 A1: X = the carrier of (R^1 | (R^1 A)) ; :: thesis: X is open
thus X is open by A1, PRE_TOPC:29; :: thesis: verum