let X be non empty addLoopStr ; :: thesis: for M, N being Subset of X
for x being Point of X st M c= N holds
x + M c= x + N
let M, N be Subset of X; :: thesis: for x being Point of X st M c= N holds
x + M c= x + N
let x be Point of X; :: thesis: ( M c= N implies x + M c= x + N )
assume A1: M c= N ; :: thesis: x + M c= x + N
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x + M or z in x + N )
assume A2: z in x + M ; :: thesis: z in x + N
then reconsider z = z as Point of X ;
x + M = { (x + u) where u is Element of X : u in M } by RUSUB_4:def 8;
then ex u being Point of X st
( x + u = z & u in M ) by A2;
hence z in x + N by A1, Lm1; :: thesis: verum