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:35;
hence ( not A is open or (R^1 (AffineMap a,b)) .: A is open ) by A2, A3, TOPGRP_1:25; :: thesis: verum