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

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