let A be Subset of (R^1 | (R^1 (dom (AffineMap (a,b))))); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or (R^1 (AffineMap (a,b))) .: A is open )
A1: b is Real by XREAL_0:def 1;
A2: R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) by Lm12;
A3: R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) by Lm12;
a is Real by XREAL_0:def 1;
then R^1 (AffineMap (a,b)) is being_homeomorphism by A1, A2, A3, JORDAN16:20;
hence ( not A is open or (R^1 (AffineMap (a,b))) .: A is open ) by A2, A3, TOPGRP_1:25; :: thesis: verum