let X be LinearTopSpace; :: thesis: for x being Point of X
for V being Subset of X holds x + (Int V) = Int (x + V)
let x be Point of X; :: thesis: for V being Subset of X holds x + (Int V) = Int (x + V)
let V be Subset of X; :: thesis: x + (Int V) = Int (x + V)
x + (Int V) c= x + V by Th8, TOPS_1:16;
hence x + (Int V) c= Int (x + V) by TOPS_1:24; :: according to XBOOLE_0:def 10 :: thesis: Int (x + V) c= x + (Int V)
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in Int (x + V) or v in x + (Int V) )
assume A1: v in Int (x + V) ; :: thesis: v in x + (Int V)
then reconsider v = v as Point of X ;
consider Q being Subset of X such that
A2: Q is open and
A3: Q c= x + V and
A4: v in Q by A1, TOPS_1:22;
(- x) + Q c= (- x) + (x + V) by A3, Th8;
then (- x) + Q c= ((- x) + x) + V by Th6;
then (- x) + Q c= (0. X) + V by RLVECT_1:5;
then (- x) + Q c= V by Th5;
then A5: ( x + (Int V) = { (x + u) where u is Point of X : u in Int V } & (- x) + Q c= Int V ) by A2, RUSUB_4:def 8, TOPS_1:24;
(- x) + v in (- x) + Q by A4, Lm1;
then x + ((- x) + v) in x + (Int V) by A5;
then (x + (- x)) + v in x + (Int V) by RLVECT_1:def 3;
then (0. X) + v in x + (Int V) by RLVECT_1:5;
hence v in x + (Int V) ; :: thesis: verum