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