let X be non empty RLTopStruct ; :: thesis: for a being Point of
for V being Subset of holds (transl a,X) .: V = a + V
let a be Point of ; :: thesis: for V being Subset of holds (transl a,X) .: V = a + V
let V be Subset of ; :: 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 set ; :: 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 such that
A1: c in V and
A2: y = (transl a,X) . c by FUNCT_2:116;
y = a + c by A2, Def10;
hence y in a + V by A1, Lm1; :: thesis: verum

end;

let x be set ; :: 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 : u in V } by RUSUB_4:def 9;
then consider u being Point of 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:43; :: thesis: verum