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: R^1 = R^1 | (R^1 (dom (AffineMap (a,b)))) by Lm12;
A2: R^1 = R^1 | (R^1 (rng (AffineMap (a,b)))) by Lm12;
R^1 (AffineMap (a,b)) is being_homeomorphism by A1, A2, JORDAN16:20;
hence ( not A is open or (R^1 (AffineMap (a,b))) .: A is open ) by A1, A2, TOPGRP_1:25; :: thesis: verum