let X be non empty RLTopStruct ; :: thesis: for a being Point of X
for V being Subset of X holds (transl (a,X)) .: V = a + V
let a be Point of X; :: thesis: for V being Subset of X holds (transl (a,X)) .: V = a + V
let V be Subset of X; :: thesis: (transl (a,X)) .: V = a + V
thus (transl (a,X)) .: V c= a + V :: according to XBOOLE_0:def 10 :: thesis: a + V c= (transl (a,X)) .: V
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (transl (a,X)) .: V or y in a + V )
assume y in (transl (a,X)) .: V ; :: thesis: y in a + V
then consider c being Point of X such that
A1: c in V and
A2: y = (transl (a,X)) . c by FUNCT_2:65;
y = a + c by A2, Def10;
hence y in a + V by A1, Lm1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a + V or x in (transl (a,X)) .: V )
assume x in a + V ; :: thesis: x in (transl (a,X)) .: V
then x in { (a + u) where u is Point of X : u in V } by RUSUB_4:def 8;
then consider u being Point of X such that
A3: x = a + u and
A4: u in V ;
x = (transl (a,X)) . u by A3, Def10;
hence x in (transl (a,X)) .: V by A4, FUNCT_2:35; :: thesis: verum