let X be non empty addLoopStr ; :: thesis: for M, N being Subset of
for x being Point of st M c= N holds
x + M c= x + N
let M, N be Subset of ; :: thesis: for x being Point of st M c= N holds
x + M c= x + N
let x be Point of ; :: thesis: ( M c= N implies x + M c= x + N )
assume A1: M c= N ; :: thesis: x + M c= x + N
let z be set ; :: 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 + M = { (x + u) where u is Element of : u in M } by RUSUB_4:def 9;
then ex u being Point of st
( x + u = z & u in M ) by A2;
hence z in x + N by A1, Lm1; :: thesis: verum