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