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 set ; :: 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 10;
then ex u, v being Point of X st
( u + v = x & u in M & v in V ) ;
then x in { (u' + v') where u', v' is Point of X : ( u' in N & v' in V ) } by A1;
hence x in N + V by RUSUB_4:def 10; :: thesis: verum